1 /-
2 Copyright (c) 2019 Seul Baek. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Author: Seul Baek
5
6 Correctness lemmas for equality elimination.
7 See 5.5 of <http://www.decision-procedures.org/> for details.
8 -/
9
10 import tactic.omega.clause
src └─────────────────┘
11
12 open list.func
13
14 namespace omega
15
16 def symdiv (i j : int) : int :=
id └─┘ └─┘
src └─┘ └─┘
typ └─┘ └─┘
17 if (2 * (i % j)) < j
id ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
18 then i / j
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
19 else (i / j) + 1
id ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴
20
21 def symmod (i j : int) : int :=
id └─┘ └─┘
src └─┘ └─┘
typ └─┘ └─┘
22 if (2 * (i % j)) < j
id ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
23 then i % j
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
24 else (i % j) - j
id ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
25
26 lemma symmod_add_one_self {i : int} :
id └─┘
src └─┘
typ └─┘
27 0 < i → symmod i (i+1) = -1 :=
id ┴ ┴ └────┘ ┴ ┴┴ ┴ ┴
src ┴ └────┘ ┴ ┴ ┴
typ ┴ ┴ └────┘ ┴ ┴┴ ┴ ┴
28 begin
st └─────
29 intro h1,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └─┘
st ─────────┘└─
30 unfold symmod,
src └───────────┘
typ └───────────┘
doc └───────────┘
txt └───────────┘
par └───────────┘
pid └─────┘
st ──────────────┘└─
31 rw [int.mod_eq_of_lt (le_of_lt h1) (lt_add_one _), if_neg],
id └──────────────┘ └──────┘ └┘ └────────┘ └────┘
src └──┘└──────────────┘┴ └──────┘┴ └┘ └────────┘└───┘└────┘┴
typ └──┘└──────────────┘┴ └──────┘┴└┘└┘ └────────┘└───┘└────┘┴
doc └──┘ ┴ ┴ └┘ └───┘ ┴
txt └──┘ ┴ ┴ └┘ └───┘ ┴
par └──┘ ┴ ┴ └┘ └───┘ ┴
pid └┘ ┴ ┴ └┘ └───┘ ┴
st ──────────────────────────────────────────────────┘└──────┘└──
32 simp only [add_comm, add_neg_cancel_left,
id └──────┘ └─────────────────┘
src └─────────┘└──────┘└┘└─────────────────┘└─
typ └─────────┘└──────┘└┘└─────────────────┘└─
doc └─────────┘ └┘ └─
txt └─────────┘ └┘ └─
par └─────────┘ └┘ └─
pid ┴└──┘└┘ └┘ └─
st ────────────────────────────────────────────
33 neg_add_rev, sub_eq_add_neg],
id └─────────┘ └────────────┘
src ───┘└─────────┘└┘└────────────┘┴
typ ───┘└─────────┘└┘└────────────┘┴
doc ───┘ └┘ ┴
txt ───┘ └┘ ┴
par ───┘ └┘ ┴
pid ───┘ └┘ ┴
st ───────────────────────────────┘└─
34 have h2 : 2 * i = (1 + 1) * i := rfl,
id ┴ ┴ ┴ ┴ └─┘
src └──────────┘┴┴ ┴┴┴ └┘┴└──┘ ┴ └──┘└─┘
typ └──────────┘┴┴ ┴┴┴ └┘┴└──┘ ┴┴└──┘└─┘
doc └──────────┘ ┴ ┴ ┴ └┘ └──┘ ┴ └──┘
txt └──────────┘ ┴ ┴ ┴ └┘ └──┘ ┴ └──┘
par └──────────┘ ┴ ┴ ┴ └┘ └──┘ ┴ └──┘
pid └─────┘└───┘ ┴ ┴ ┴ └┘ └──┘ ┴ └──┘
st ─────────────────────────────────────┘└─
35 simpa only [h2, add_mul, one_mul,
id └┘ └─────┘ └─────┘
src └──────────┘ └┘└─────┘└┘└─────┘└─
typ └──────────┘└┘└┘└─────┘└┘└─────┘└─
doc └──────────┘ └┘ └┘ └─
txt └──────────┘ └┘ └┘ └─
par └──────────┘ └┘ └┘ └─
pid ┴└──┘└┘ └┘ └┘ └─
st ────────────────────────────────────
36 add_lt_add_iff_left, not_lt] using h1
id └─────────────────┘ └────┘ └┘
src ───┘└─────────────────┘└┘└────┘└──────┘ ┴
typ ───┘└─────────────────┘└┘└────┘└──────┘└┘┴
doc ───┘ └┘ └──────┘ ┴
txt ───┘ └┘ └──────┘ ┴
par ───┘ └┘ └──────┘ ┴
pid ───┘ └┘ ┴┴└────┘ ┴
st ─────────────────────────────────────────┘
37 end
st └─┘
38
39 lemma mul_symdiv_eq {i j : int} :
id └─┘
src └─┘
typ └─┘
40 j * (symdiv i j) = i - (symmod i j) :=
id ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴
src ┴ └────┘ ┴ ┴ └────┘
typ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴
41 begin
st └─────
42 unfold symdiv, unfold symmod,
src └───────────┘ └───────────┘
typ └───────────┘ └───────────┘
doc └───────────┘ └───────────┘
txt └───────────┘ └───────────┘
par └───────────┘ └───────────┘
pid └─────┘ └─────┘
st ──────────────┘└─────────────┘└─
43 by_cases h1 : (2 * (i % j)) < j,
id ┴ ┴ ┴ ┴ ┴
src └───────┘ └─┘ └┘┴┴ ┴┴┴ └─┘┴┴
typ └───────┘ └─┘ └┘┴┴ ┴┴┴┴ └─┘┴┴┴
doc └───────┘ └─┘ └┘ ┴ ┴ ┴ └─┘ ┴
txt └───────┘ └─┘ └┘ ┴ ┴ ┴ └─┘ ┴
par └───────┘ └─┘ └┘ ┴ ┴ ┴ └─┘ ┴
pid ┴ └─┘ └┘ ┴ ┴ ┴ └─┘ ┴
st ────────────────────────────────┘└─
44 { repeat {rw if_pos h1},
id └────┘ └┘
src └──────┘└─┘└────┘┴ ┴
typ └──────┘└─┘└────┘┴└┘┴
doc └──────┘└─┘ ┴ ┴
txt └──────┘└─┘ ┴ ┴
par └──────┘└─┘ ┴ ┴
pid └───┘ ┴ ┴
st ───┘└──────────────────┘└┘└
45 rw [int.mod_def, sub_sub_cancel] },
id └─────────┘ └────────────┘
src └──┘└─────────┘└┘└────────────┘└┘
typ └──┘└─────────┘└┘└────────────┘└┘
doc └──┘ └┘ └┘
txt └──┘ └┘ └┘
par └──┘ └┘ └┘
pid └┘ └┘ ┴┴
st ──────────────────┘└──────────────┘┴┴└┘└
46 { repeat {rw if_neg h1},
id └────┘ └┘
src └──────┘└─┘└────┘┴ ┴
typ └──────┘└─┘└────┘┴└┘┴
doc └──────┘└─┘ ┴ ┴
txt └──────┘└─┘ ┴ ┴
par └──────┘└─┘ ┴ ┴
pid └───┘ ┴ ┴
st ───────────────────────┘└┘└
47 rw [int.mod_def, sub_sub, sub_sub_cancel,
id └─────────┘ └─────┘ └────────────┘
src └──┘└─────────┘└┘└─────┘└┘└────────────┘└─
typ └──┘└─────────┘└┘└─────┘└┘└────────────┘└─
doc └──┘ └┘ └┘ └─
txt └──┘ └┘ └┘ └─
par └──┘ └┘ └┘ └─
pid └┘ └┘ └┘ └─
st ──────────────────┘└───────┘└──────────────┘└─
48 mul_add, mul_one] }
id └─────┘ └─────┘
src ─────┘└─────┘└┘└─────┘└┘
typ ─────┘└─────┘└┘└─────┘└┘
doc ─────┘ └┘ └┘
txt ─────┘ └┘ └┘
par ─────┘ └┘ └┘
pid ─────┘ └┘ ┴┴
st ────────────┘└───────┘┴┴└─
49 end
st ──┘
50
51 lemma symmod_eq {i j : int} :
id └─┘
src └─┘
typ └─┘
52 symmod i j = i - j * (symdiv i j) :=
id └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴
src └────┘ ┴ ┴ ┴ └────┘
typ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴
53 by rw [mul_symdiv_eq, sub_sub_cancel]
id └───────────┘ └────────────┘
src └──┘└───────────┘└┘└────────────┘└─
typ └──┘└───────────┘└┘└────────────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └────────────────┘└──────────────┘┴└
54
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
55 /- (sgm v b as n) is the new value assigned to the nth variable
src ────────────────────────────────────────────────────────────────
typ ────────────────────────────────────────────────────────────────
doc ────────────────────────────────────────────────────────────────
txt ────────────────────────────────────────────────────────────────
par ────────────────────────────────────────────────────────────────
pid ────────────────────────────────────────────────────────────────
st ────────────────────────────────────────────────────────────────
56 after a single step of equality elimination using valuation v,
src ──────────────────────────────────────────────────────────────────
typ ──────────────────────────────────────────────────────────────────
doc ──────────────────────────────────────────────────────────────────
txt ──────────────────────────────────────────────────────────────────
par ──────────────────────────────────────────────────────────────────
pid ──────────────────────────────────────────────────────────────────
st ──────────────────────────────────────────────────────────────────
57 term ⟨b, as⟩, and variable index n. If v satisfies the initial
src ──────────────────────────────────────────────────────────────────
typ ──────────────────────────────────────────────────────────────────
doc ──────────────────────────────────────────────────────────────────
txt ──────────────────────────────────────────────────────────────────
par ──────────────────────────────────────────────────────────────────
pid ──────────────────────────────────────────────────────────────────
st ──────────────────────────────────────────────────────────────────
58 constraint set, then (v ⟨n ↦ sgm v b as n⟩) satisfies the new
src ─────────────────────────────────────────────────────────────────
typ ─────────────────────────────────────────────────────────────────
doc ─────────────────────────────────────────────────────────────────
txt ─────────────────────────────────────────────────────────────────
par ─────────────────────────────────────────────────────────────────
pid ─────────────────────────────────────────────────────────────────
st ─────────────────────────────────────────────────────────────────
59 constraint set after equality elimination. -/
src ────────────────────────────────────────────────┘
typ ────────────────────────────────────────────────┘
doc ────────────────────────────────────────────────┘
txt ────────────────────────────────────────────────┘
par ────────────────────────────────────────────────┘
pid ────────────────────────────────────────────────┘
st ────────────────────────────────────────────────┘
60 def sgm (v : nat → int) (b : int) (as : list int) (n : nat) :=
id └─┘ └─┘ └─┘ └──┘ └─┘ └─┘
src └─┘ └─┘ └─┘ └──┘ └─┘ └─┘
typ └─┘ └─┘ └─┘ └──┘ └─┘ └─┘
61 let a_n : int := get n as in
id └─┘ └─┘ ┴ └┘
src └─┘ └─┘
typ └─┘ └─┘ ┴ └┘
62 let m : int := a_n + 1 in
id └─┘ └─┘ ┴
src └─┘ ┴
typ └─┘ └─┘ ┴
63 ((symmod b m) + (coeffs.val v (as.map (λ x, symmod x m)))) / m
id └────┘ ┴ ┴ ┴ └────────┘ ┴ └┘└──┘ ┴ └────┘ ┴ ┴ ┴ ┴
src └────┘ ┴ └────────┘ └──┘ └────┘ ┴
typ └────┘ ┴ ┴ ┴ └────────┘ ┴ └┘└──┘ ┴ └────┘ ┴ ┴ ┴ ┴
64
65 open_locale list.func
66
67 def rhs : nat → int → list int → term
id └─┘ ┴ └─┘ └──┘ └─┘ └──┘
src └─┘ └─┘ └──┘ └─┘ └──┘
typ └─┘ ┴ └─┘ └──┘ └─┘ └──┘
68 | n b as :=
id ┴ ┴ └┘
typ ┴ ┴ └┘
69 let m := get n as + 1 in
id ┴ └─┘ ┴
src └─┘ ┴
typ ┴ └─┘ ┴
70 ⟨(symmod b m), (as.map (λ x, symmod x m)) {n ↦ -m}⟩
id └────┘ ┴ └──┘ ┴ └────┘ ┴ ┴ ┴ ┴ ┴┴┴
src └────┘ └──┘ └────┘ ┴ ┴ ┴ ┴
typ └────┘ ┴ └──┘ ┴ └────┘ ┴ ┴ ┴ ┴ ┴┴┴
71
72 lemma rhs_correct_aux {v : nat → int} {m : int} {as : list int} :
id └─┘ └─┘ └─┘ └──┘ └─┘
src └─┘ └─┘ └─┘ └──┘ └─┘
typ └─┘ └─┘ └─┘ └──┘ └─┘
73 ∀ {k}, ∃ d, (m * d +
id ┴┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴┴ ┴ ┴┴ ┴ ┴ ┴ ┴
74 coeffs.val_between v (as.map (λ (x : ℤ), symmod x m)) 0 k =
id └────────────────┘ ┴ └┘└──┘ ┴ └────┘ ┴ ┴ ┴ ┴
src └────────────────┘ └──┘ ┴ └────┘ ┴
typ └────────────────┘ ┴ └┘└──┘ ┴ └────┘ ┴ ┴ ┴ ┴
75 coeffs.val_between v as 0 k)
id └────────────────┘ ┴ └┘ ┴
src └────────────────┘
typ └────────────────┘ ┴ └┘ ┴
76 | 0 :=
77 begin
st └─────
78 existsi (0 : int),
id └─┘
src └──────┘ └──┘└─┘┴
typ └──────┘ └──┘└─┘┴
doc └──────┘ └──┘ ┴
txt └──────┘ └──┘ ┴
par └──────┘ └──┘ ┴
pid ┴ └──┘ ┴
st ────────────────────┘└─
79 simp only [add_zero, mul_zero, coeffs.val_between]
id └──────┘ └──────┘ └────────────────┘
src └─────────┘└──────┘└┘└──────┘└┘└────────────────┘└─
typ └─────────┘└──────┘└┘└──────┘└┘└────────────────┘└─
doc └─────────┘ └┘ └┘ └─
txt └─────────┘ └┘ └┘ └─
par └─────────┘ └┘ └┘ └─
pid ┴└──┘└┘ └┘ └┘ ┴└
st ───────────────────────────────────────────────────────
80 end
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
81 | (k+1) :=
id ┴
src ┴
typ ┴
82 begin
st └─────
83 simp only [zero_add, coeffs.val_between, list.map],
id └──────┘ └────────────────┘ └──────┘
src └─────────┘└──────┘└┘└────────────────┘└┘└──────┘┴
typ └─────────┘└──────┘└┘└────────────────┘└┘└──────┘┴
doc └─────────┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ ┴
st ─────────────────────────────────────────────────────┘└─
84 cases @rhs_correct_aux k with d h1, rw ← h1,
id └─────────────┘ ┴ └┘
src └────┘ ┴ └────────┘ └───┘
typ └────┘ └─────────────┘┴┴└────────┘ └───┘└┘
doc └────┘ ┴ └────────┘ └───┘
txt └────┘ ┴ └────────┘ └───┘
par └────┘ ┴ └────────┘ └───┘
pid ┴ ┴ └────────┘ └─┘
st ─────────────────────────────────────┘└───────┘└─
85 by_cases hk : k < as.length,
id ┴ ┴ └───────┘
src └───────┘ └─┘ ┴┴┴└───────┘
typ └───────┘ └─┘┴┴┴┴└───────┘
doc └───────┘ └─┘ ┴ ┴
txt └───────┘ └─┘ ┴ ┴
par └───────┘ └─┘ ┴ ┴
pid ┴ └─┘ ┴ ┴
st ──────────────────────────────┘└─
86 { rw [get_map hk, symmod_eq, sub_mul],
id └─────┘ └┘ └───────┘ └─────┘
src └──┘└─────┘┴ └┘└───────┘└┘└─────┘┴
typ └──┘└─────┘┴└┘└┘└───────┘└┘└─────┘┴
doc └──┘ ┴ └┘ └┘ ┴
txt └──┘ ┴ └┘ └┘ ┴
par └──┘ ┴ └┘ └┘ ┴
pid └┘ ┴ └┘ └┘ ┴
st ─────┘└────────────┘└─────────┘└───────┘└──
87 existsi (d + (symdiv (get k as) m * v k)),
id ┴ ┴ └────┘ └─┘ └┘ ┴ ┴ ┴ ┴
src └──────┘ ┴┴┴ └────┘┴ └─┘┴ ┴ └┘ ┴┴┴ ┴ └┘
typ └──────┘ ┴┴┴┴ └────┘┴ └─┘┴ ┴└┘└┘┴┴┴┴┴┴┴└┘
doc └──────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘
txt └──────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘
par └──────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘
pid ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘
st ──────────────────────────────────────────────┘└─
88 ring },
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ──────────┘└┘└
89 { rw not_lt at hk,
id └────┘
src └─┘└────┘└────┘
typ └─┘└────┘└────┘
doc └─┘ └────┘
txt └─┘ └────┘
par └─┘ └────┘
pid ┴ └────┘
st ────────────────────┘└─
90 repeat {rw get_eq_default_of_le},
id └──────────────────┘
src └──────┘└─┘└──────────────────┘┴
typ └──────┘└─┘└──────────────────┘┴
doc └──────┘└─┘ ┴
txt └──────┘└─┘ ┴
par └──────┘└─┘ ┴
pid └───┘ ┴
st ────────────────────────────────────┘└┘└
91 existsi d,
id ┴
src └──────┘
typ └──────┘┴
doc └──────┘
txt └──────┘
par └──────┘
pid ┴
st ──────────────┘└─
92 rw add_assoc,
id └───────┘
src └─┘└───────┘
typ └─┘└───────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ─────────────────┘└─
93 exact hk,
id └┘
src └────┘
typ └────┘└┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────┘└─
94 simp only [hk, list.length_map] }
id └┘ └─────────────┘
src └─────────┘ └┘└─────────────┘└┘
typ └─────────┘└┘└┘└─────────────┘└┘
doc └─────────┘ └┘ └┘
txt └─────────┘ └┘ └┘
par └─────────┘ └┘ └┘
pid ┴└──┘└┘ └┘ ┴┴
st ─────────────────────────────────────┘└─
95 end
st ────┘
96
97 open_locale omega
98
99 lemma rhs_correct {v : nat → int}
id └─┘ └─┘
src └─┘ └─┘
typ └─┘ └─┘
100 {b : int} {as : list int} (n : nat) :
id └─┘ └──┘ └─┘ └─┘
src └─┘ └──┘ └─┘ └─┘
typ └─┘ └──┘ └─┘ └─┘
101 0 < get n as →
id ┴ └─┘ ┴ └┘
src ┴ └─┘
typ ┴ └─┘ ┴ └┘
102 0 = term.val v (b,as) →
id ┴ └──────┘ ┴ ┴┴ └┘
src ┴ └──────┘ ┴
typ ┴ └──────┘ ┴ ┴┴ └┘
103 v n = term.val (v ⟨n ↦ sgm v b as n⟩) (rhs n b as) :=
id ┴ ┴ ┴ └──────┘ ┴ ┴┴ ┴ └─┘ ┴ ┴ └┘ ┴┴ └─┘ ┴ ┴ └┘
src ┴ └──────┘ ┴ ┴ └─┘ ┴ └─┘
typ ┴ ┴ ┴ └──────┘ ┴ ┴┴ ┴ └─┘ ┴ ┴ └┘ ┴┴ └─┘ ┴ ┴ └┘
104 begin
st └─────
105 intros h0 h1,
src └──────────┘
typ └──────────┘
doc └──────────┘
txt └──────────┘
par └──────────┘
pid └────┘
st ─────────────┘└─
106 let a_n := get n as,
id └─┘ ┴ └┘
src └─────────┘└─┘┴ ┴
typ └─────────┘└─┘┴┴┴└┘
doc └─────────┘ ┴ ┴
txt └─────────┘ ┴ ┴
par └─────────┘ ┴ ┴
pid └─────┘┴└─┘ ┴ ┴
st ────────────────────┘└─
107 let m := a_n + 1,
id └─┘ ┴
src └───────┘ ┴┴└┘
typ └───────┘└─┘┴┴└┘
doc └───────┘ ┴ └┘
txt └───────┘ ┴ └┘
par └───────┘ ┴ └┘
pid └───┘┴└─┘ ┴ ┴┴
st ─────────────────┘└─
108 have h3 : m ≠ 0,
id ┴ ┴
src └────────┘ ┴┴└┘
typ └────────┘┴┴┴└┘
doc └────────┘ ┴ └┘
txt └────────┘ ┴ └┘
par └────────┘ ┴ └┘
pid └─────┘└─┘ ┴ ┴┴
st ────────────────┘└─
109 { apply ne_of_gt, apply lt_trans h0, simp [a_n, m] },
id └──────┘ └──────┘ └┘ └─┘ ┴
src └────┘└──────┘ └────┘└──────┘┴ └────┘ └┘ └┘
typ └────┘└──────┘ └────┘└──────┘┴└┘ └────┘└─┘└┘┴└┘
doc └────┘ └────┘ ┴ └────┘ └┘ └┘
txt └────┘ └────┘ ┴ └────┘ └┘ └┘
par └────┘ └────┘ ┴ └────┘ └┘ └┘
pid ┴ ┴ ┴ ┴┴ └┘ ┴┴
st ───┘└────────────┘└─────────────────┘└──────────────┘└┘└
110 have h2 : m * (sgm v b as n) = (symmod b m) +
id ┴ └─┘ ┴ ┴ ┴
src └────────┘ ┴┴┴ └─┘┴ ┴ ┴ ┴ └┘┴┴ ┴ ┴ └┘ └
typ └────────┘ ┴┴┴ └─┘┴ ┴ ┴ ┴┴└┘┴┴ ┴┴┴ └┘ └
doc └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ └
txt └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ └
par └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ └
pid └─────┘└─┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ └
st ────────────────────────────────────────────────
111 coeffs.val v (as.map (λ x, symmod x m)),
id └────────┘ ┴ └────┘ └────┘ ┴
src ───┘└────────┘┴ ┴ └────┘┴ └──┘└────┘┴ ┴ └┘
typ ───┘└────────┘┴┴┴ └────┘┴ └──┘└────┘┴ ┴┴└┘
doc ───┘ ┴ ┴ ┴ └──┘ ┴ ┴ └┘
txt ───┘ ┴ ┴ ┴ └──┘ ┴ ┴ └┘
par ───┘ ┴ ┴ ┴ └──┘ ┴ ┴ └┘
pid ───┘ ┴ ┴ ┴ └──┘ ┴ ┴ └┘
st ──────────────────────────────────────────┘└─
112 { simp only [sgm, mul_comm m],
id └─┘ └──────┘ ┴
src └─────────┘└─┘└┘└──────┘┴ ┴
typ └─────────┘└─┘└┘└──────┘┴┴┴
doc └─────────┘ └┘ ┴ ┴
txt └─────────┘ └┘ ┴ ┴
par └─────────┘ └┘ ┴ ┴
pid ┴└──┘└┘ └┘ ┴ ┴
st ───┘└─────────────────────────┘└─
113 rw [int.div_mul_cancel],
id └────────────────┘
src └──┘└────────────────┘┴
typ └──┘└────────────────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st ─────────────────────────┘└──
114 have h4 : ∃ c, m * c + (symmod b (get n as + 1) +
id ┴ ┴ └─┘ ┴
src └────────┘┴└┘┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘┴ ┴ ┴ └──┘ └
typ └────────┘┴└┘┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘┴┴┴ ┴ └──┘ └
doc └────────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └
txt └────────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └
par └────────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └
pid └─────┘└─┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └
st ──────────────────────────────────────────────────────
115 coeffs.val v (as.map (λ (x : ℤ), symmod x m))) = term.val v (b,as),
id └────────┘ └────┘ └────┘ ┴ └──────┘ ┴ ┴┴ └┘
src ─────┘└────────┘┴ ┴ └────┘┴ └────┘ └─┘└────┘┴ ┴ └──┘ ┴└──────┘┴ ┴┴ ┴ ┴
typ ─────┘└────────┘┴ ┴ └────┘┴ └────┘ └─┘└────┘┴ ┴┴└──┘ ┴└──────┘┴┴┴┴┴┴└┘┴
doc ─────┘ ┴ ┴ ┴ └────┘ └─┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
txt ─────┘ ┴ ┴ ┴ └────┘ └─┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
par ─────┘ ┴ ┴ ┴ └────┘ └─┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
pid ─────┘ ┴ ┴ ┴ └────┘ └─┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
st ───────────────────────────────────────────────────────────────────────┘└─
116 { have h5: ∃ d, m * d +
id ┴ ┴
src └───────┘┴└┘┴└┘ ┴ ┴ ┴ └
typ └───────┘┴└┘┴└┘ ┴ ┴ ┴ └
doc └───────┘ └┘ └┘ ┴ ┴ ┴ └
txt └───────┘ └┘ └┘ ┴ ┴ ┴ └
par └───────┘ └┘ └┘ ┴ ┴ ┴ └
pid └─────┘└┘ └┘ └┘ ┴ ┴ ┴ └
st ─────┘└──────────────────────
117 (coeffs.val v (as.map (λ x, symmod x m))) = coeffs.val v as,
id └────┘ └────┘ ┴ └────────┘ ┴ └┘
src ───────┘ ┴ ┴ └────┘┴ └──┘└────┘┴ ┴ └──┘ ┴└────────┘┴ ┴
typ ───────┘ ┴ ┴ └────┘┴ └──┘└────┘┴ ┴┴└──┘ ┴└────────┘┴┴┴└┘
doc ───────┘ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ ┴
txt ───────┘ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ ┴
par ───────┘ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ ┴
pid ───────┘ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ ┴
st ──────────────────────────────────────────────────────────────────┘└─
118 { simp only [coeffs.val, list.length_map], apply rhs_correct_aux },
id └────────┘ └─────────────┘ └─────────────┘
src └─────────┘└────────┘└┘└─────────────┘┴ └────┘└─────────────┘┴
typ └─────────┘└────────┘└┘└─────────────┘┴ └────┘└─────────────┘┴
doc └─────────┘ └┘ ┴ └────┘ ┴
txt └─────────┘ └┘ ┴ └────┘ ┴
par └─────────┘ └┘ ┴ └────┘ ┴
pid ┴└──┘└┘ └┘ ┴ ┴ ┴
st ───────┘└─────────────────────────────────────┘└──────────────────────┘└┘└
119 cases h5 with d h5, rw symmod_eq,
id └┘ └───────┘
src └────┘ └────────┘ └─┘└───────┘
typ └────┘└┘└────────┘ └─┘└───────┘
doc └────┘ └────────┘ └─┘
txt └────┘ └────────┘ └─┘
par └────┘ └────────┘ └─┘
pid ┴ └────────┘ ┴
st ───────────────────────┘└────────────┘└─
120 existsi (symdiv b m + d),
id └────┘ ┴ ┴ ┴
src └──────┘ └────┘┴ ┴ ┴ ┴ ┴
typ └──────┘ └────┘┴┴┴┴┴ ┴┴┴
doc └──────┘ ┴ ┴ ┴ ┴ ┴
txt └──────┘ ┴ ┴ ┴ ┴ ┴
par └──────┘ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴ ┴
st ─────────────────────────────┘└─
121 unfold term.val, rw ← h5,
id └┘
src └─────────────┘ └───┘
typ └─────────────┘ └───┘└┘
doc └─────────────┘ └───┘
txt └─────────────┘ └───┘
par └─────────────┘ └───┘
pid └───────┘ └─┘
st ────────────────────┘└───────┘└─
122 simp only [term.val, mul_add, add_mul, m, a_n],
id └──────┘ └─────┘ └─────┘ ┴ └─┘
src └─────────┘└──────┘└┘└─────┘└┘└─────┘└┘ └┘ ┴
typ └─────────┘└──────┘└┘└─────┘└┘└─────┘└┘┴└┘└─┘┴
doc └─────────┘ └┘ └┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ └┘ └┘ ┴
st ───────────────────────────────────────────────────┘└─
123 ring },
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ──────────┘└┘└
124 cases h4 with c h4,
id └┘
src └────┘ └────────┘
typ └────┘└┘└────────┘
doc └────┘ └────────┘
txt └────┘ └────────┘
par └────┘ └────────┘
pid ┴ └────────┘
st ─────────────────────┘└─
125 rw [dvd_add_iff_right (dvd_mul_right m c), h4, ← h1],
id └───────────────┘ └───────────┘ ┴ ┴ └┘ └┘
src └──┘└───────────────┘┴ └───────────┘┴ ┴ └─┘ └──┘ ┴
typ └──┘└───────────────┘┴ └───────────┘┴┴┴┴└─┘└┘└──┘└┘┴
doc └──┘ ┴ ┴ ┴ └─┘ └──┘ ┴
txt └──┘ ┴ ┴ ┴ └─┘ └──┘ ┴
par └──┘ ┴ ┴ ┴ └─┘ └──┘ ┴
pid └┘ ┴ ┴ ┴ └─┘ └──┘ ┴
st ────────────────────────────────────────────┘└──┘└────┘└──
126 apply dvd_zero },
id └──────┘
src └────┘└──────┘┴
typ └────┘└──────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ──────────────────┘└┘└
127 apply calc v n
src └────┘ ┴ ┴ └
typ └────┘ ┴ ┴ └
doc └────┘ ┴ ┴ └
txt └────┘ ┴ ┴ └
par └────┘ ┴ ┴ └
pid ┴ ┴ ┴ └
st ─────────────────
128 = -(m * sgm v b as n) + (symmod b m) +
id ┴
src ─────┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ └
typ ─────┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ └
doc ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ └
txt ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ └
par ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ └
pid ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ └
st ─────────────────────────────────────────────
129 (coeffs.val_except n v (as.map (λ x, symmod x m))) :
id └───────────────┘ └────┘ └────┘ ┴
src ───────┘ └───────────────┘┴ ┴ ┴ └────┘┴ └──┘└────┘┴ ┴ └─────
typ ───────┘ └───────────────┘┴ ┴ ┴ └────┘┴ └──┘└────┘┴ ┴┴└─────
doc ───────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └─────
txt ───────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └─────
par ───────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └─────
pid ───────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └─────
st ─────────────────────────────────────────────────────────────
130 begin
src ───────┘ └
typ ───────┘ └
doc ───────┘ └
txt ───────┘ └
par ───────┘ └
pid ───────┘ └
st ───────┘└─────
131 rw [h2, ← coeffs.val_except_add_eq n],
id └┘ └──────────────────────┘ ┴
src ─────────┘└──┘ └──┘└──────────────────────┘┴ ┴└─
typ ─────────┘└──┘└┘└──┘└──────────────────────┘┴┴┴└─
doc ─────────┘└──┘ └──┘ ┴ ┴└─
txt ─────────┘└──┘ └──┘ ┴ ┴└─
par ─────────┘└──┘ └──┘ ┴ ┴└─
pid ─────────────┘ └──┘ ┴ └──
st ───────────────┘└────────────────────────────┘└──
132 have hn : n < as.length,
id ┴ ┴ └───────┘
src ─────────┘└────────┘ ┴┴┴└───────┘└─
typ ─────────┘└────────┘┴┴┴┴└───────┘└─
doc ─────────┘└────────┘ ┴ ┴ └─
txt ─────────┘└────────┘ ┴ ┴ └─
par ─────────┘└────────┘ ┴ ┴ └─
pid ───────────────────┘ ┴ ┴ └─
st ────────────────────────────────┘└─
133 { by_contra hc, rw not_lt at hc,
id └────┘
src ───────────┘└──────────┘└┘└─┘└────┘└────┘└─
typ ───────────┘└──────────┘└┘└─┘└────┘└────┘└─
doc ───────────┘└──────────┘└┘└─┘ └────┘└─
txt ───────────┘└──────────┘└┘└─┘ └────┘└─
par ───────────┘└──────────┘└┘└─┘ └────┘└─
pid ────────────────────────────┘ └───────
st ──────────┘└───────────┘└───────────────┘└─
134 rw (get_eq_default_of_le n hc) at h0,
id └──────────────────┘ ┴ └┘
src ───────────┘└─┘ └──────────────────┘┴ ┴ └─────┘└─
typ ───────────┘└─┘ └──────────────────┘┴┴┴└┘└─────┘└─
doc ───────────┘└─┘ ┴ ┴ └─────┘└─
txt ───────────┘└─┘ ┴ ┴ └─────┘└─
par ───────────┘└─┘ ┴ ┴ └─────┘└─
pid ──────────────┘ ┴ ┴ └────────
st ───────────────────────────────────────────────┘└─
135 cases h0 },
id └┘
src ───────────┘└────┘ ┴└──
typ ───────────┘└────┘└┘┴└──
doc ───────────┘└────┘ ┴└──
txt ───────────┘└────┘ ┴└──
par ───────────┘└────┘ ┴└──
pid ─────────────────┘ └───
st ────────────────────┘┴└─
136 rw get_map hn,
id └─────┘ └┘
src ─────────┘└─┘└─────┘┴ └─
typ ─────────┘└─┘└─────┘┴└┘└─
doc ─────────┘└─┘ ┴ └─
txt ─────────┘└─┘ ┴ └─
par ─────────┘└─┘ ┴ └─
pid ────────────┘ ┴ └─
st ──────────────────────┘└─
137 simp only [a_n, m],
id └─┘ ┴
src ─────────┘└─────────┘ └┘ ┴└─
typ ─────────┘└─────────┘└─┘└┘┴┴└─
doc ─────────┘└─────────┘ └┘ ┴└─
txt ─────────┘└─────────┘ └┘ ┴└─
par ─────────┘└─────────┘ └┘ ┴└─
pid ────────────────────┘ └┘ └──
st ───────────────────────────┘└─
138 rw [add_comm, symmod_add_one_self h0],
id └──────┘ └─────────────────┘ └┘
src ─────────┘└──┘└──────┘└┘└─────────────────┘┴ ┴└─
typ ─────────┘└──┘└──────┘└┘└─────────────────┘┴└┘┴└─
doc ─────────┘└──┘ └┘ ┴ ┴└─
txt ─────────┘└──┘ └┘ ┴ ┴└─
par ─────────┘└──┘ └┘ ┴ ┴└─
pid ─────────────┘ └┘ ┴ └──
st ─────────────────────┘└──────────────────────┘└──
139 ring
src ─────────┘└────
typ ─────────┘└────
doc ─────────┘└────
txt ─────────┘└────
par ─────────┘└────
pid ───────────────
st ───────────────
140 end
src ───────┘└───
typ ───────┘└───
doc ───────┘└───
txt ───────┘└───
par ───────┘└───
pid ────────────
st ───────┘└─┘└
141 ... = term.val (v⟨n↦sgm v b as n⟩) (rhs n b as) :
id └──────┘ ┴ └─┘ └─┘ ┴ ┴ └┘
src ─────┘ ┴└──────┘┴ └─┘┴ ┴ ┴ ┴ └┘ └─┘┴ ┴ ┴ └───
typ ─────┘ ┴└──────┘┴ ┴ └─┘┴ ┴ ┴ ┴ └┘ └─┘┴┴┴┴┴└┘└───
doc ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └───
txt ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └───
par ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └───
pid ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └───
st ────────────────────────────────────────────────────
142 begin
src ───────┘ └
typ ───────┘ └
doc ───────┘ └
txt ───────┘ └
par ───────┘ └
pid ───────┘ └
st ───────┘└─────
143 unfold rhs, unfold term.val,
src ─────────┘└────────┘└┘└─────────────┘└─
typ ─────────┘└────────┘└┘└─────────────┘└─
doc ─────────┘└────────┘└┘└─────────────┘└─
txt ─────────┘└────────┘└┘└─────────────┘└─
par ─────────┘└────────┘└┘└─────────────┘└─
pid ───────────────────────────────────────
st ───────────────────┘└───────────────┘└─
144 rw [← coeffs.val_except_add_eq n, get_set, update_eq],
id └──────────────────────┘ ┴ └─────┘ └───────┘
src ─────────┘└────┘└──────────────────────┘┴ └┘└─────┘└┘└───────┘┴└─
typ ─────────┘└────┘└──────────────────────┘┴┴└┘└─────┘└┘└───────┘┴└─
doc ─────────┘└────┘ ┴ └┘ └┘ ┴└─
txt ─────────┘└────┘ ┴ └┘ └┘ ┴└─
par ─────────┘└────┘ ┴ └┘ └┘ ┴└─
pid ───────────────┘ ┴ └┘ └┘ └──
st ─────────────────────────────────────────┘└───────┘└─────────┘└──
145 have h2 : ∀ a b c : int, a + b + c = b + (c + a) := by {intros, ring},
id └─┘
src ─────────┘└────────┘ └───────┘└─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ └┘└────┘└┘└──┘┴└─
typ ─────────┘└────────┘ └───────┘└─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ └┘└────┘└┘└──┘┴└─
doc ─────────┘└────────┘ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ └┘└────┘└┘└──┘┴└─
txt ─────────┘└────────┘ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ └┘└────┘└┘└──┘┴└─
par ─────────┘└────────┘ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ └┘└────┘└┘└──┘┴└─
pid ───────────────────┘ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ └────────────────
st ───────────────────────────────────────────────────────────────┘└──────┘└────┘┴└─
146 rw (h2 (- _)),
id └┘
src ─────────┘└─┘ ┴ └──┘└─
typ ─────────┘└─┘ └┘┴ └──┘└─
doc ─────────┘└─┘ ┴ └──┘└─
txt ─────────┘└─┘ ┴ └──┘└─
par ─────────┘└─┘ ┴ └──┘└─
pid ────────────┘ ┴ └─────
st ──────────────────────┘└─
147 apply fun_mono_2 rfl,
id └────────┘ └─┘
src ───────────────┘└────────┘┴└─┘└─
typ ───────────────┘└────────┘┴└─┘└─
doc ───────────────┘ ┴ └─
txt ───────────────┘ ┴ └─
par ───────────────┘ ┴ └─
pid ───────────────┘ ┴ └─
st ─────────────────────────────┘└─
148 apply fun_mono_2,
id └────────┘
src ───────────────┘└────────┘└─
typ ───────────────┘└────────┘└─
doc ───────────────┘ └─
txt ───────────────┘ └─
par ───────────────┘ └─
pid ───────────────┘ └─
st ─────────────────────────┘└─
149 { rw coeffs.val_except_update_set },
id └──────────────────────────┘
src ───────────┘└─┘└──────────────────────────┘┴└──
typ ───────────┘└─┘└──────────────────────────┘┴└──
doc ───────────┘└─┘ ┴└──
txt ───────────┘└─┘ ┴└──
par ───────────┘└─┘ ┴└──
pid ──────────────┘ └───
st ──────────┘└───────────────────────────────┘┴└─
150 { simp only [m, a_n], ring }
id ┴ └─┘
src ───────────┘└─────────┘ └┘ ┴└┘└───┘└─
typ ───────────┘└─────────┘┴└┘└─┘┴└┘└───┘└─
doc ───────────┘└─────────┘ └┘ ┴└┘└───┘└─
txt ───────────┘└─────────┘ └┘ ┴└┘└───┘└─
par ───────────┘└─────────┘ └┘ ┴└┘└───┘└─
pid ──────────────────────┘ └┘ └─────────
st ─────────────────────────────┘└─────┘└─
151 end
src ───────────┘
typ ───────────┘
doc ───────────┘
txt ───────────┘
par ───────────┘
pid ──────────┘┴
st ──────────┘┴
152 end
st └─┘
153
154 def sym_sym (m b : int) : int :=
id └─┘ └─┘
src └─┘ └─┘
typ └─┘ └─┘
155 symdiv b m + symmod b m
id └────┘ ┴ ┴ ┴ └────┘ ┴ ┴
src └────┘ ┴ └────┘
typ └────┘ ┴ ┴ ┴ └────┘ ┴ ┴
156
157 def coeffs_reduce : nat → int → list int → term
id └─┘ ┴ └─┘ └──┘ └─┘ └──┘
src └─┘ └─┘ └──┘ └─┘ └──┘
typ └─┘ ┴ └─┘ └──┘ └─┘ └──┘
158 | n b as :=
id ┴ ┴ └┘
typ ┴ ┴ └┘
159 let a := get n as in
id ┴ └─┘
src └─┘
typ ┴ └─┘
160 let m := a + 1 in
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
161 (sym_sym m b, (as.map (sym_sym m)) {n ↦ -a})
id ┴└─────┘ ┴ └──┘ └─────┘ ┴ ┴ ┴ ┴┴┴
src ┴└─────┘ └──┘ └─────┘ ┴ ┴ ┴ ┴
typ ┴└─────┘ ┴ └──┘ └─────┘ ┴ ┴ ┴ ┴┴┴
162
163 lemma coeffs_reduce_correct
164 {v : nat → int} {b : int} {as : list int} {n : nat} :
id └─┘ └─┘ └─┘ └──┘ └─┘ └─┘
src └─┘ └─┘ └─┘ └──┘ └─┘ └─┘
typ └─┘ └─┘ └─┘ └──┘ └─┘ └─┘
165 0 < get n as →
id ┴ └─┘ ┴ └┘
src ┴ └─┘
typ ┴ └─┘ ┴ └┘
166 0 = term.val v (b,as) →
id ┴ └──────┘ ┴ ┴┴ └┘
src ┴ └──────┘ ┴
typ ┴ └──────┘ ┴ ┴┴ └┘
167 0 = term.val (v ⟨n ↦ sgm v b as n⟩) (coeffs_reduce n b as) :=
id ┴ └──────┘ ┴ ┴┴ ┴ └─┘ ┴ ┴ └┘ ┴┴ └───────────┘ ┴ ┴ └┘
src ┴ └──────┘ ┴ ┴ └─┘ ┴ └───────────┘
typ ┴ └──────┘ ┴ ┴┴ ┴ └─┘ ┴ ┴ └┘ ┴┴ └───────────┘ ┴ ┴ └┘
168 begin
st └─────
169 intros h1 h2,
src └──────────┘
typ └──────────┘
doc └──────────┘
txt └──────────┘
par └──────────┘
pid └────┘
st ─────────────┘└─
170 let a_n := get n as,
id └─┘ ┴ └┘
src └─────────┘└─┘┴ ┴
typ └─────────┘└─┘┴┴┴└┘
doc └─────────┘ ┴ ┴
txt └─────────┘ ┴ ┴
par └─────────┘ ┴ ┴
pid └─────┘┴└─┘ ┴ ┴
st ────────────────────┘└─
171 let m := a_n + 1,
id └─┘ ┴
src └───────┘ ┴┴└┘
typ └───────┘└─┘┴┴└┘
doc └───────┘ ┴ └┘
txt └───────┘ ┴ └┘
par └───────┘ ┴ └┘
pid └───┘┴└─┘ ┴ ┴┴
st ─────────────────┘└─
172 have h3 : m ≠ 0,
id ┴ ┴
src └────────┘ ┴┴└┘
typ └────────┘┴┴┴└┘
doc └────────┘ ┴ └┘
txt └────────┘ ┴ └┘
par └────────┘ ┴ └┘
pid └─────┘└─┘ ┴ ┴┴
st ────────────────┘└─
173 { apply ne_of_gt,
id └──────┘
src └────┘└──────┘
typ └────┘└──────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───┘└────────────┘└─
174 apply lt_trans h1,
id └──────┘ └┘
src └────┘└──────┘┴
typ └────┘└──────┘┴└┘
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ────────────────────┘└─
175 simp only [m, lt_add_iff_pos_right] },
id ┴ └──────────────────┘
src └─────────┘ └┘└──────────────────┘└┘
typ └─────────┘┴└┘└──────────────────┘└┘
doc └─────────┘ └┘ └┘
txt └─────────┘ └┘ └┘
par └─────────┘ └┘ └┘
pid ┴└──┘└┘ └┘ ┴┴
st ───────────────────────────────────────┘└┘└
176 have h4 : 0 = (term.val (v⟨n↦sgm v b as n⟩) (coeffs_reduce n b as)) * m :=
id ┴ └──────┘ ┴ └─┘ └───────────┘ ┴ ┴ └┘ ┴ ┴
src └──────────┘┴┴ └──────┘┴ └─┘┴ ┴ ┴ ┴ └┘ └───────────┘┴ ┴ ┴ └─┘┴┴ └───
typ └──────────┘┴┴ └──────┘┴ ┴ └─┘┴ ┴ ┴ ┴ └┘ └───────────┘┴┴┴┴┴└┘└─┘┴┴┴└───
doc └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ └───
txt └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ └───
par └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ └───
pid └─────┘└───┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ └───
st ─────────────────────────────────────────────────────────────────────────────
177 calc 0
src ─┘ └───
typ ─┘ └───
doc ─┘ └───
txt ─┘ └───
par ─┘ └───
pid ─┘ └───
st ──────────
178 = term.val v (b,as) : h2
id └──────┘ ┴ ┴┴ └┘ └┘
src ─────┘ ┴└──────┘┴ ┴┴ ┴ └──┘ └
typ ─────┘ ┴└──────┘┴┴┴┴┴┴└┘└──┘└┘└
doc ─────┘ ┴ ┴ ┴ ┴ └──┘ └
txt ─────┘ ┴ ┴ ┴ ┴ └──┘ └
par ─────┘ ┴ ┴ ┴ ┴ └──┘ └
pid ─────┘ ┴ ┴ ┴ ┴ └──┘ └
st ───────────────────────────────
179 ... = b + coeffs.val_except n v as
id └───────────────┘
src ─────┘ ┴ ┴ ┴└───────────────┘┴ ┴ ┴ └
typ ─────┘ ┴ ┴ ┴└───────────────┘┴ ┴ ┴ └
doc ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └
txt ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └
par ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └
pid ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └
st ─────────────────────────────────────
180 + a_n * ((rhs n b as).val (v⟨n ↦ sgm v b as n⟩)) :
id └─┘ └─┘ └─┘ ┴
src ─────────┘ ┴ ┴ ┴ └─┘┴ ┴ ┴ └────┘ ┴ ┴└─┘┴ ┴ ┴ ┴ └────
typ ─────────┘ ┴└─┘┴ ┴ └─┘┴ ┴ ┴ └────┘ ┴ ┴└─┘┴ ┴ ┴ ┴┴ └────
doc ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────
txt ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────
par ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────
pid ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────
st ─────────────────────────────────────────────────────────────
181 begin
src ───────┘ └
typ ───────┘ └
doc ───────┘ └
txt ───────┘ └
par ───────┘ └
pid ───────┘ └
st ───────┘└─────
182 unfold term.val,
src ─────────┘└─────────────┘└─
typ ─────────┘└─────────────┘└─
doc ─────────┘└─────────────┘└─
txt ─────────┘└─────────────┘└─
par ─────────┘└─────────────┘└─
pid ───────────────────────────
st ────────────────────────┘└─
183 rw [← coeffs.val_except_add_eq n, rhs_correct n h1 h2],
id └──────────────────────┘ ┴ └─────────┘ ┴ └┘ └┘
src ─────────┘└────┘└──────────────────────┘┴ └┘└─────────┘┴ ┴ ┴ ┴└─
typ ─────────┘└────┘└──────────────────────┘┴┴└┘└─────────┘┴┴┴└┘┴└┘┴└─
doc ─────────┘└────┘ ┴ └┘ ┴ ┴ ┴ ┴└─
txt ─────────┘└────┘ ┴ └┘ ┴ ┴ ┴ ┴└─
par ─────────┘└────┘ ┴ └┘ ┴ ┴ ┴ ┴└─
pid ───────────────┘ ┴ └┘ ┴ ┴ ┴ └──
st ─────────────────────────────────────────┘└───────────────────┘└──
184 simp only [a_n, add_assoc],
id └─┘ └───────┘
src ─────────┘└─────────┘ └┘└───────┘┴└─
typ ─────────┘└─────────┘└─┘└┘└───────┘┴└─
doc ─────────┘└─────────┘ └┘ ┴└─
txt ─────────┘└─────────┘ └┘ ┴└─
par ─────────┘└─────────┘ └┘ ┴└─
pid ────────────────────┘ └┘ └──
st ───────────────────────────────────┘└─
185 end
src ────────────
typ ────────────
doc ────────────
txt ────────────
par ────────────
pid ────────────
st ──────────┘└
186 ... = -(m * a_n * sgm v b as n) + (b + a_n * (symmod b m)) +
src ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └
typ ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └
doc ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └
txt ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └
par ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └
pid ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └
st ───────────────────────────────────────────────────────────────
187 (coeffs.val_except n v as +
src ───────┘ ┴ ┴ ┴ ┴ └
typ ───────┘ ┴ ┴ ┴ ┴ └
doc ───────┘ ┴ ┴ ┴ ┴ └
txt ───────┘ ┴ ┴ ┴ ┴ └
par ───────┘ ┴ ┴ ┴ ┴ └
pid ───────┘ ┴ ┴ ┴ ┴ └
st ────────────────────────────────────
188 a_n * coeffs.val_except n v (as.map (λ x, symmod x m))) :
id └────┘ └────┘ ┴
src ───────┘ ┴ ┴ ┴ ┴ ┴ └────┘┴ └──┘└────┘┴ ┴ └─────
typ ───────┘ ┴ ┴ ┴ ┴ ┴ └────┘┴ └──┘└────┘┴ ┴┴└─────
doc ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └─────
txt ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └─────
par ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └─────
pid ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └─────
st ──────────────────────────────────────────────────────────────────
189 begin
src ─────────┘ └
typ ─────────┘ └
doc ─────────┘ └
txt ─────────┘ └
par ─────────┘ └
pid ─────────┘ └
st ─────────┘└─────
190 simp only [term.val, rhs, mul_add, m, a_n,
id └──────┘ └─┘ └─────┘ ┴ └─┘
src ───────────┘└─────────┘└──────┘└┘└─┘└┘└─────┘└┘ └┘ └─
typ ───────────┘└─────────┘└──────┘└┘└─┘└┘└─────┘└┘┴└┘└─┘└─
doc ───────────┘└─────────┘ └┘ └┘ └┘ └┘ └─
txt ───────────┘└─────────┘ └┘ └┘ └┘ └┘ └─
par ───────────┘└─────────┘ └┘ └┘ └┘ └┘ └─
pid ──────────────────────┘ └┘ └┘ └┘ └┘ └─
st ───────────────────────────────────────────────────────
191 add_assoc, add_left_inj, add_comm, add_left_comm],
id └───────┘ └──────────┘ └──────┘ └───────────┘
src ─────────────┘└───────┘└┘└──────────┘└┘└──────┘└┘└───────────┘┴└─
typ ─────────────┘└───────┘└┘└──────────┘└┘└──────┘└┘└───────────┘┴└─
doc ─────────────┘ └┘ └┘ └┘ ┴└─
txt ─────────────┘ └┘ └┘ └┘ ┴└─
par ─────────────┘ └┘ └┘ └┘ ┴└─
pid ─────────────┘ └┘ └┘ └┘ └──
st ──────────────────────────────────────────────────────────────┘└─
192 rw [← coeffs.val_except_add_eq n,
id └──────────────────────┘ ┴
src ───────────┘└────┘└──────────────────────┘┴ └─
typ ───────────┘└────┘└──────────────────────┘┴┴└─
doc ───────────┘└────┘ ┴ └─
txt ───────────┘└────┘ ┴ └─
par ───────────┘└────┘ ┴ └─
pid ─────────────────┘ ┴ └─
st ───────────────────────────────────────────┘└─
193 get_set, update_eq, mul_add],
id └─────┘ └───────┘ └─────┘
src ─────────────┘└─────┘└┘└───────┘└┘└─────┘┴└─
typ ─────────────┘└─────┘└┘└───────┘└┘└─────┘┴└─
doc ─────────────┘ └┘ └┘ ┴└─
txt ─────────────┘ └┘ └┘ ┴└─
par ─────────────┘ └┘ └┘ ┴└─
pid ─────────────┘ └┘ └┘ └──
st ────────────────────┘└─────────┘└───────┘└──
194 apply fun_mono_2,
id └────────┘
src ───────────┘└────┘└────────┘└─
typ ───────────┘└────┘└────────┘└─
doc ───────────┘└────┘ └─
txt ───────────┘└────┘ └─
par ───────────┘└────┘ └─
pid ─────────────────┘ └─
st ───────────────────────────┘└─
195 { rw coeffs.val_except_eq_val_except
id └─────────────────────────────┘
src ─────────────┘└─┘└─────────────────────────────┘└
typ ─────────────┘└─┘└─────────────────────────────┘└
doc ─────────────┘└─┘ └
txt ─────────────┘└─┘ └
par ─────────────┘└─┘ └
pid ────────────────┘ └
st ────────────┘└───────────────────────────────────
196 update_eq_of_ne (get_set_eq_of_ne _) },
id └─────────────┘ └──────────────┘
src ─────────────┘└─────────────┘┴ └──────────────┘└──┘└──
typ ─────────────┘└─────────────┘┴ └──────────────┘└──┘└──
doc ─────────────┘ ┴ └──┘└──
txt ─────────────┘ ┴ └──┘└──
par ─────────────┘ ┴ └──┘└──
pid ─────────────┘ ┴ └──────
st ──────────────────────────────────────────────────┘┴└─
197 simp only [m], ring,
id ┴
src ───────────┘└─────────┘ ┴└┘└──┘└─
typ ───────────┘└─────────┘┴┴└┘└──┘└─
doc ───────────┘└─────────┘ ┴└┘└──┘└─
txt ───────────┘└─────────┘ ┴└┘└──┘└─
par ───────────┘└─────────┘ ┴└┘└──┘└─
pid ──────────────────────┘ └────────
st ────────────────────────┘└────┘└─
198 end
src ──────────────
typ ──────────────
doc ──────────────
txt ──────────────
par ──────────────
pid ──────────────
st ────────────┘└
199 ... = -(m * a_n * sgm v b as n) + (b + a_n * (symmod b m))
src ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
typ ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
doc ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
txt ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
par ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
pid ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
st ─────────────────────────────────────────────────────────────
200 + coeffs.val_except n v (as.map (λ a_i, a_i + a_n * (symmod a_i m))) :
src ───────┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────
typ ───────┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────
doc ───────┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────
txt ───────┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────
par ───────┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────
pid ───────┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────
st ───────────────────────────────────────────────────────────────────────────────
201 begin
src ───────┘ └
typ ───────┘ └
doc ───────┘ └
txt ───────┘ └
par ───────┘ └
pid ───────┘ └
st ───────┘└─────
202 apply fun_mono_2 rfl,
id └────────┘ └─┘
src ─────────┘└────┘└────────┘┴└─┘└─
typ ─────────┘└────┘└────────┘┴└─┘└─
doc ─────────┘└────┘ ┴ └─
txt ─────────┘└────┘ ┴ └─
par ─────────┘└────┘ ┴ └─
pid ───────────────┘ ┴ └─
st ─────────────────────────────┘└─
203 simp only [coeffs.val_except, mul_add],
id └───────────────┘ └─────┘
src ─────────┘└─────────┘└───────────────┘└┘└─────┘┴└─
typ ─────────┘└─────────┘└───────────────┘└┘└─────┘┴└─
doc ─────────┘└─────────┘ └┘ ┴└─
txt ─────────┘└─────────┘ └┘ ┴└─
par ─────────┘└─────────┘ └┘ ┴└─
pid ────────────────────┘ └┘ └──
st ───────────────────────────────────────────────┘└─
204 repeat {rw ← coeffs.val_between_map_mul},
id └────────────────────────┘
src ─────────┘└──────┘└───┘└────────────────────────┘┴└─
typ ─────────┘└──────┘└───┘└────────────────────────┘┴└─
doc ─────────┘└──────┘└───┘ ┴└─
txt ─────────┘└──────┘└───┘ ┴└─
par ─────────┘└──────┘└───┘ ┴└─
pid ──────────────────────┘ └──
st ────────────────────────────────────────────────┘┴└─
205 have h4 : ∀ {a b c d : int},
id └─┘
src ───────────────────┘ └──────────┘└─┘┴ └
typ ───────────────────┘ └──────────┘└─┘┴ └
doc ───────────────────┘ └──────────┘ ┴ └
txt ───────────────────┘ └──────────┘ ┴ └
par ───────────────────┘ └──────────┘ ┴ └
pid ───────────────────┘ └──────────┘ ┴ └
st ───────────────────────────────────────
206 a + b + (c + d) = (a + c) + (b + d),
src ───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └──
typ ───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └──
doc ───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └──
txt ───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └──
par ───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └──
pid ───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └──
st ──────────────────────────────────────────────┘└─
207 { intros, ring }, rw h4,
src ───────────┘└────┘└┘└───┘└─┘└─┘ └─
typ ───────────┘└────┘└┘└───┘└─┘└─┘└┘└─
doc ───────────┘└────┘└┘└───┘└─┘└─┘ └─
txt ───────────┘└────┘└┘└───┘└─┘└─┘ └─
par ───────────┘└────┘└┘└───┘└─┘└─┘ └─
pid ──────────────────────────────┘ └─
st ──────────┘└─────┘└─────┘┴└─────┘└─
208 have h5 : add as (list.map (has_mul.mul a_n)
id └─┘ └─────────┘
src ───────────────────┘└─┘┴ ┴ ┴ └─────────┘┴ └─
typ ───────────────────┘└─┘┴ ┴ ┴ └─────────┘┴ └─
doc ───────────────────┘ ┴ ┴ ┴ ┴ └─
txt ───────────────────┘ ┴ ┴ ┴ ┴ └─
par ───────────────────┘ ┴ ┴ ┴ ┴ └─
pid ───────────────────┘ ┴ ┴ ┴ ┴ └─
st ───────────────────────────────────────────────────────
209 (list.map (λ (x : ℤ), symmod x (get n as + 1)) as)) =
id └─┘ ┴
src ───────────┘ ┴ └────┘ └─┘ ┴ ┴ └─┘┴ ┴ ┴ └───┘ └─┘ └
typ ───────────┘ ┴ └────┘ └─┘ ┴ ┴ └─┘┴┴┴ ┴ └───┘ └─┘ └
doc ───────────┘ ┴ └────┘ └─┘ ┴ ┴ ┴ ┴ ┴ └───┘ └─┘ └
txt ───────────┘ ┴ └────┘ └─┘ ┴ ┴ ┴ ┴ ┴ └───┘ └─┘ └
par ───────────┘ ┴ └────┘ └─┘ ┴ ┴ ┴ ┴ ┴ └───┘ └─┘ └
pid ───────────┘ ┴ └────┘ └─┘ ┴ ┴ ┴ ┴ ┴ └───┘ └─┘ └
st ──────────────────────────────────────────────────────────────────
210 list.map (λ (a_i : ℤ), a_i + a_n * symmod a_i m) as,
id └──────┘ └─┘ └────┘ ┴ └┘
src ───────────┘└──────┘┴ └──────┘ └─┘ ┴ ┴ ┴ ┴└────┘┴ ┴ └┘ └─
typ ───────────┘└──────┘┴ └──────┘ └─┘ ┴ ┴└─┘┴ ┴└────┘┴ ┴┴└┘└┘└─
doc ───────────┘ ┴ └──────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └─
txt ───────────┘ ┴ └──────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └─
par ───────────┘ ┴ └──────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └─
pid ───────────┘ ┴ └──────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └─
st ──────────────────────────────────────────────────────────────┘└─
211 { rw [list.map_map, ←map_add_map],
id └──────────┘ └─────────┘
src ───────────┘└──┘└──────────┘└─┘└─────────┘┴└─
typ ───────────┘└──┘└──────────┘└─┘└─────────┘┴└─
doc ───────────┘└──┘ └─┘ ┴└─
txt ───────────┘└──┘ └─┘ ┴└─
par ───────────┘└──┘ └─┘ ┴└─
pid ───────────────┘ └─┘ └──
st ──────────┘└───────────────┘└────────────┘└──
212 apply fun_mono_2,
id └────────┘
src ───────────┘└────┘└────────┘└─
typ ───────────┘└────┘└────────┘└─
doc ───────────┘└────┘ └─
txt ───────────┘└────┘ └─
par ───────────┘└────┘ └─
pid ─────────────────┘ └─
st ───────────────────────────┘└─
213 { have h5 : (λ x : int, x) = id,
id └─┘ └┘
src ───────────────────────┘ └───┘└─┘└┘ └┘ ┴└┘└─
typ ───────────────────────┘ └───┘└─┘└┘ └┘ ┴└┘└─
doc ───────────────────────┘ └───┘ └┘ └┘ ┴ └─
txt ───────────────────────┘ └───┘ └┘ └┘ ┴ └─
par ───────────────────────┘ └───┘ └┘ └┘ ┴ └─
pid ───────────────────────┘ └───┘ └┘ └┘ ┴ └─
st ────────────┘└────────────────────────────┘└─
214 { rw function.funext_iff, intro x, refl },
id └─────────────────┘
src ───────────────┘└─┘└─────────────────┘└┘└─────┘└┘└───┘└──
typ ───────────────┘└─┘└─────────────────┘└┘└─────┘└┘└───┘└──
doc ───────────────┘└─┘ └┘└─────┘└┘└───┘└──
txt ───────────────┘└─┘ └┘└─────┘└┘└───┘└──
par ───────────────┘└─┘ └┘└─────┘└┘└───┘└──
pid ──────────────────┘ └──────────────────
st ──────────────┘└─────────────────────┘└───────┘└─────┘┴└─
215 rw [h5, list.map_id] },
id └┘ └─────────┘
src ─────────────┘└──┘ └┘└─────────┘└┘└──
typ ─────────────┘└──┘└┘└┘└─────────┘└┘└──
doc ─────────────┘└──┘ └┘ └┘└──
txt ─────────────┘└──┘ └┘ └┘└──
par ─────────────┘└──┘ └┘ └┘└──
pid ─────────────────┘ └┘ └────
st ───────────────────┘└───────────┘┴┴┴└─
216 { apply fun_mono_2 _ rfl,
id └────────┘ └─┘
src ─────────────┘└────┘└────────┘└─┘└─┘└─
typ ─────────────┘└────┘└────────┘└─┘└─┘└─
doc ─────────────┘└────┘ └─┘ └─
txt ─────────────┘└────┘ └─┘ └─
par ─────────────┘└────┘ └─┘ └─
pid ───────────────────┘ └─┘ └─
st ───────────────────────────────────┘└─
217 rw function.funext_iff, intro x,
id └─────────────────┘
src ─────────────┘└─┘└─────────────────┘└┘└─────┘└─
typ ─────────────┘└─┘└─────────────────┘└┘└─────┘└─
doc ─────────────┘└─┘ └┘└─────┘└─
txt ─────────────┘└─┘ └┘└─────┘└─
par ─────────────┘└─┘ └┘└─────┘└─
pid ────────────────┘ └──────────
st ───────────────────────────────────┘└───────┘└─
218 simp only [m] } },
id ┴
src ─────────────┘└─────────┘ └┘└────
typ ─────────────┘└─────────┘┴└┘└────
doc ─────────────┘└─────────┘ └┘└────
txt ─────────────┘└─────────┘ └┘└────
par ─────────────┘└─────────┘ └┘└────
pid ────────────────────────┘ └──────
st ───────────────────────────┘└─┘└─
219 simp only [list.length_map],
id └─────────────┘
src ─────────┘└─────────┘└─────────────┘┴└─
typ ─────────┘└─────────┘└─────────────┘┴└─
doc ─────────┘└─────────┘ ┴└─
txt ─────────┘└─────────┘ ┴└─
par ─────────┘└─────────┘ ┴└─
pid ────────────────────┘ └──
st ────────────────────────────────────┘└─
220 repeat { rw [← coeffs.val_between_add, h5] },
id └────────────────────┘ └┘
src ─────────┘└───────┘└────┘└────────────────────┘└┘ └┘┴└─
typ ─────────┘└───────┘└────┘└────────────────────┘└┘└┘└┘┴└─
doc ─────────┘└───────┘└────┘ └┘ └┘┴└─
txt ─────────┘└───────┘└────┘ └┘ └┘┴└─
par ─────────┘└───────┘└────┘ └┘ └┘┴└─
pid ────────────────────────┘ └┘ └────
st ──────────────────────────────────────────────┘└──┘┴┴┴└─
221 end
src ────────────
typ ────────────
doc ────────────
txt ────────────
par ────────────
pid ────────────
st ──────────┘└
222 ... = -(m * a_n * sgm v b as n) + (m * sym_sym m b)
src ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └─
typ ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └─
doc ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └─
txt ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └─
par ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └─
pid ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └─
st ──────────────────────────────────────────────────────
223 + coeffs.val_except n v (as.map (λ a_i, m * sym_sym m a_i)) :
id └─────┘
src ───────┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴└─────┘┴ ┴ └────
typ ───────┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴└─────┘┴ ┴ └────
doc ───────┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ └────
txt ───────┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ └────
par ───────┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ └────
pid ───────┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ └────
st ──────────────────────────────────────────────────────────────────────
224 begin
src ───────┘ └
typ ───────┘ └
doc ───────┘ └
txt ───────┘ └
par ───────┘ └
pid ───────┘ └
st ───────┘└─────
225 repeat {rw add_assoc}, apply fun_mono_2, refl,
id └───────┘ └────────┘
src ─────────┘└──────┘└─┘└───────┘┴└┘└────┘└────────┘└┘└──┘└─
typ ─────────┘└──────┘└─┘└───────┘┴└┘└────┘└────────┘└┘└──┘└─
doc ─────────┘└──────┘└─┘ ┴└┘└────┘ └┘└──┘└─
txt ─────────┘└──────┘└─┘ ┴└┘└────┘ └┘└──┘└─
par ─────────┘└──────┘└─┘ ┴└┘└────┘ └┘└──┘└─
pid ────────────────────┘ └───────┘ └───────
st ─────────────────────────────┘┴└────────────────┘└────┘└─
226 rw ← add_assoc,
id └───────┘
src ─────────┘└───┘└───────┘└─
typ ─────────┘└───┘└───────┘└─
doc ─────────┘└───┘ └─
txt ─────────┘└───┘ └─
par ─────────┘└───┘ └─
pid ──────────────┘ └─
st ───────────────────────┘└─
227 have h4 : ∀ (x : ℤ), x + a_n * symmod x m = m * sym_sym m x,
id └─┘ └────┘ └─────┘ ┴
src ───────────────────┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴└────┘┴ ┴ ┴ ┴ ┴ ┴└─────┘┴ ┴ └─
typ ───────────────────┘ └────┘ ┴ ┴ ┴ ┴└─┘┴ ┴└────┘┴ ┴ ┴ ┴ ┴ ┴└─────┘┴┴┴ └─
doc ───────────────────┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─
txt ───────────────────┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─
par ───────────────────┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─
pid ───────────────────┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─
st ────────────────────────────────────────────────────────────────────┘└─
228 { intro x, have h5 : a_n = m - 1,
id └─┘ ┴ ┴
src ───────────┘└─────┘└──────────┘ ┴ ┴ ┴┴└───
typ ───────────┘└─────┘└──────────┘└─┘┴ ┴┴┴┴└───
doc ───────────┘└─────┘└──────────┘ ┴ ┴ ┴ └───
txt ───────────┘└─────┘└──────────┘ ┴ ┴ ┴ └───
par ───────────┘└─────┘└──────────┘ ┴ ┴ ┴ └───
pid ──────────────────────────────┘ ┴ ┴ ┴ └───
st ──────────┘└──────┘└─────────────────────┘└─
229 { simp only [m],
id ┴
src ─────────────┘└─────────┘ ┴└─
typ ─────────────┘└─────────┘┴┴└─
doc ─────────────┘└─────────┘ ┴└─
txt ─────────────┘└─────────┘ ┴└─
par ─────────────┘└─────────┘ ┴└─
pid ────────────────────────┘ └──
st ────────────┘└────────────┘└─
230 rw add_sub_cancel },
id └────────────┘
src ─────────────┘└─┘└────────────┘┴└──
typ ─────────────┘└─┘└────────────┘┴└──
doc ─────────────┘└─┘ ┴└──
txt ─────────────┘└─┘ ┴└──
par ─────────────┘└─┘ ┴└──
pid ────────────────┘ └───
st ───────────────────────────────┘┴└─
231 rw [h5, sub_mul, one_mul, add_sub,
id └┘ └─────┘ └─────┘ └─────┘
src ───────────┘└──┘ └┘└─────┘└┘└─────┘└┘└─────┘└─
typ ───────────┘└──┘└┘└┘└─────┘└┘└─────┘└┘└─────┘└─
doc ───────────┘└──┘ └┘ └┘ └┘ └─
txt ───────────┘└──┘ └┘ └┘ └┘ └─
par ───────────┘└──┘ └┘ └┘ └┘ └─
pid ───────────────┘ └┘ └┘ └┘ └─
st ─────────────────┘└───────┘└───────┘└───────┘└─
232 add_comm, add_sub_assoc, ← mul_symdiv_eq],
id └──────┘ └───────────┘ └───────────┘
src ─────────────┘└──────┘└┘└───────────┘└──┘└───────────┘┴└─
typ ─────────────┘└──────┘└┘└───────────┘└──┘└───────────┘┴└─
doc ─────────────┘ └┘ └──┘ ┴└─
txt ─────────────┘ └┘ └──┘ ┴└─
par ─────────────┘ └┘ └──┘ ┴└─
pid ─────────────┘ └┘ └──┘ └──
st ─────────────────────┘└─────────────┘└───────────────┘└──
233 simp only [sym_sym, mul_add, add_comm] },
id └─────┘ └─────┘ └──────┘
src ───────────┘└─────────┘└─────┘└┘└─────┘└┘└──────┘└┘└──
typ ───────────┘└─────────┘└─────┘└┘└─────┘└┘└──────┘└┘└──
doc ───────────┘└─────────┘ └┘ └┘ └┘└──
txt ───────────┘└─────────┘ └┘ └┘ └┘└──
par ───────────┘└─────────┘ └┘ └┘ └┘└──
pid ──────────────────────┘ └┘ └┘ └────
st ──────────────────────────────────────────────────┘┴└─
234 apply fun_mono_2 (h4 _),
id └────────┘ └┘
src ─────────┘└────┘└────────┘┴ └─┘└─
typ ─────────┘└────┘└────────┘┴ └┘└─┘└─
doc ─────────┘└────┘ ┴ └─┘└─
txt ─────────┘└────┘ ┴ └─┘└─
par ─────────┘└────┘ ┴ └─┘└─
pid ───────────────┘ ┴ └────
st ────────────────────────────────┘└─
235 apply coeffs.val_except_eq_val_except; intros x h5, refl,
id └─────────────────────────────┘
src ─────────┘└────┘└─────────────────────────────┘└┘└─────────┘└┘└──┘└─
typ ─────────┘└────┘└─────────────────────────────┘└┘└─────────┘└┘└──┘└─
doc ─────────┘└────┘ └┘└─────────┘└┘└──┘└─
txt ─────────┘└────┘ └┘└─────────┘└┘└──┘└─
par ─────────┘└────┘ └┘└─────────┘└┘└──┘└─
pid ───────────────┘ └────────────────────
st ───────────────────────────────────────────────────────────┘└────┘└─
236 apply congr_arg,
id └───────┘
src ─────────┘└────┘└───────┘└─
typ ─────────┘└────┘└───────┘└─
doc ─────────┘└────┘ └─
txt ─────────┘└────┘ └─
par ─────────┘└────┘ └─
pid ───────────────┘ └─
st ────────────────────────┘└─
237 apply fun_mono_2 _ rfl,
id └────────┘ └─┘
src ─────────┘└────┘└────────┘└─┘└─┘└─
typ ─────────┘└────┘└────────┘└─┘└─┘└─
doc ─────────┘└────┘ └─┘ └─
txt ─────────┘└────┘ └─┘ └─
par ─────────┘└────┘ └─┘ └─
pid ───────────────┘ └─┘ └─
st ───────────────────────────────┘└─
238 rw function.funext_iff,
id └─────────────────┘
src ─────────┘└─┘└─────────────────┘└─
typ ─────────┘└─┘└─────────────────┘└─
doc ─────────┘└─┘ └─
txt ─────────┘└─┘ └─
par ─────────┘└─┘ └─
pid ────────────┘ └─
st ───────────────────────────────┘└─
239 apply h4
src ─────────┘└────┘ └
typ ─────────┘└────┘ └
doc ─────────┘└────┘ └
txt ─────────┘└────┘ └
par ─────────┘└────┘ └
pid ───────────────┘ └
st ───────────────────
240 end
src ───────┘└───
typ ───────┘└───
doc ───────┘└───
txt ───────┘└───
par ───────┘└───
pid ────────────
st ───────┘└─┘└
241 ... = (-(a_n * sgm v b as n) + (sym_sym m b)
src ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─
typ ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─
doc ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─
txt ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─
par ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─
pid ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─
st ───────────────────────────────────────────────
242 + coeffs.val_except n v (as.map (sym_sym m))) * m :
src ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └──
typ ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └──
doc ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └──
txt ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └──
par ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └──
pid ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └──
st ────────────────────────────────────────────────────────────
243 begin
src ───────┘ └
typ ───────┘ └
doc ───────┘ └
txt ───────┘ └
par ───────┘ └
pid ───────┘ └
st ───────┘└─────
244 simp only [add_mul _ _ m],
id └─────┘ ┴
src ─────────┘└─────────┘└─────┘└───┘ ┴└─
typ ─────────┘└─────────┘└─────┘└───┘┴┴└─
doc ─────────┘└─────────┘ └───┘ ┴└─
txt ─────────┘└─────────┘ └───┘ ┴└─
par ─────────┘└─────────┘ └───┘ ┴└─
pid ────────────────────┘ └───┘ └──
st ──────────────────────────────────┘└─
245 apply fun_mono_2, ring,
id └────────┘
src ─────────┘└────┘└────────┘└┘└──┘└─
typ ─────────┘└────┘└────────┘└┘└──┘└─
doc ─────────┘└────┘ └┘└──┘└─
txt ─────────┘└────┘ └┘└──┘└─
par ─────────┘└────┘ └┘└──┘└─
pid ───────────────┘ └───────
st ─────────────────────────┘└────┘└─
246 simp only [coeffs.val_except, add_mul _ _ m],
id └───────────────┘ └─────┘ ┴
src ─────────┘└─────────┘└───────────────┘└┘└─────┘└───┘ ┴└─
typ ─────────┘└─────────┘└───────────────┘└┘└─────┘└───┘┴┴└─
doc ─────────┘└─────────┘ └┘ └───┘ ┴└─
txt ─────────┘└─────────┘ └┘ └───┘ ┴└─
par ─────────┘└─────────┘ └┘ └───┘ ┴└─
pid ────────────────────┘ └┘ └───┘ └──
st ─────────────────────────────────────────────────────┘└─
247 apply fun_mono_2,
id └────────┘
src ─────────┘└────┘└────────┘└─
typ ─────────┘└────┘└────────┘└─
doc ─────────┘└────┘ └─
txt ─────────┘└────┘ └─
par ─────────┘└────┘ └─
pid ───────────────┘ └─
st ─────────────────────────┘└─
248 { rw [mul_comm _ m, ← coeffs.val_between_map_mul, list.map_map] },
id └──────┘ ┴ └────────────────────────┘ └──────────┘
src ───────────┘└──┘└──────┘└─┘ └──┘└────────────────────────┘└┘└──────────┘└┘└──
typ ───────────┘└──┘└──────┘└─┘┴└──┘└────────────────────────┘└┘└──────────┘└┘└──
doc ───────────┘└──┘ └─┘ └──┘ └┘ └┘└──
txt ───────────┘└──┘ └─┘ └──┘ └┘ └┘└──
par ───────────┘└──┘ └─┘ └──┘ └┘ └┘└──
pid ───────────────┘ └─┘ └──┘ └┘ └────
st ──────────┘└───────────────┘└────────────────────────────┘└────────────┘┴┴┴└─
249 simp only [list.length_map, mul_comm _ m],
id └─────────────┘ └──────┘ ┴
src ─────────┘└─────────┘└─────────────┘└┘└──────┘└─┘ ┴└─
typ ─────────┘└─────────┘└─────────────┘└┘└──────┘└─┘┴┴└─
doc ─────────┘└─────────┘ └┘ └─┘ ┴└─
txt ─────────┘└─────────┘ └┘ └─┘ ┴└─
par ─────────┘└─────────┘ └┘ └─┘ ┴└─
pid ────────────────────┘ └┘ └─┘ └──
st ──────────────────────────────────────────────────┘└─
250 rw [← coeffs.val_between_map_mul, list.map_map]
id └────────────────────────┘ └──────────┘
src ─────────┘└────┘└────────────────────────┘└┘└──────────┘└─
typ ─────────┘└────┘└────────────────────────┘└┘└──────────┘└─
doc ─────────┘└────┘ └┘ └─
txt ─────────┘└────┘ └┘ └─
par ─────────┘└────┘ └┘ └─
pid ───────────────┘ └┘ └─
st ─────────────────────────────────────────┘└────────────┘┴└
251 end
src ───────┘└───
typ ───────┘└───
doc ───────┘└───
txt ───────┘└───
par ───────┘└───
pid ────────────
st ───────┘└─┘└
252 ... = (sym_sym m b + (coeffs.val_except n v (as.map (sym_sym m)) +
src ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └
typ ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └
doc ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └
txt ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └
par ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └
pid ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └
st ─────────────────────────────────────────────────────────────────────
253 (-a_n * sgm v b as n))) * m : by ring
id ┴
src ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └─┘ ┴└────
typ ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └─┘ ┴└────
doc ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └─┘ ┴└────
txt ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └─┘ ┴└────
par ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └─┘ ┴└────
pid ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └─┘ └─────
st ─────────────────────────────────────────┘└─────
254 ... = (term.val (v ⟨n ↦ sgm v b as n⟩) (coeffs_reduce n b as)) * m :
id └───────────┘
src ─┘└──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └───────────┘┴ ┴ ┴ └─┘ ┴ └──
typ ─┘└──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └───────────┘┴ ┴ ┴ └─┘ ┴ └──
doc ─┘└──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ └──
txt ─┘└──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ └──
par ─┘└──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ └──
pid ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ └──
st ─┘└────────────────────────────────────────────────────────────────────
255 begin
src ───────┘ └
typ ───────┘ └
doc ───────┘ └
txt ───────┘ └
par ───────┘ └
pid ───────┘ └
st ───────┘└─────
256 simp only [coeffs_reduce, term.val, m, a_n],
id └───────────┘ └──────┘ ┴ └─┘
src ─────────┘└─────────┘└───────────┘└┘└──────┘└┘ └┘ ┴└─
typ ─────────┘└─────────┘└───────────┘└┘└──────┘└┘┴└┘└─┘┴└─
doc ─────────┘└─────────┘ └┘ └┘ └┘ ┴└─
txt ─────────┘└─────────┘ └┘ └┘ └┘ ┴└─
par ─────────┘└─────────┘ └┘ └┘ └┘ ┴└─
pid ────────────────────┘ └┘ └┘ └┘ └──
st ────────────────────────────────────────────────────┘└─
257 rw [← coeffs.val_except_add_eq n,
id └──────────────────────┘ ┴
src ─────────┘└────┘└──────────────────────┘┴ └─
typ ─────────┘└────┘└──────────────────────┘┴┴└─
doc ─────────┘└────┘ ┴ └─
txt ─────────┘└────┘ ┴ └─
par ─────────┘└────┘ ┴ └─
pid ───────────────┘ ┴ └─
st ─────────────────────────────────────────┘└─
258 coeffs.val_except_update_set, get_set, update_eq]
id └──────────────────────────┘ └─────┘ └───────┘
src ───────────┘└──────────────────────────┘└┘└─────┘└┘└───────┘└─
typ ───────────┘└──────────────────────────┘└┘└─────┘└┘└───────┘└─
doc ───────────┘ └┘ └┘ └─
txt ───────────┘ └┘ └┘ └─
par ───────────┘ └┘ └┘ └─
pid ───────────┘ └┘ └┘ └─
st ───────────────────────────────────────┘└───────┘└─────────┘┴└
259 end,
src ───────┘└─┘
typ ───────┘└─┘
doc ───────┘└─┘
txt ───────┘└─┘
par ───────┘└─┘
pid ──────────┘
st ───────┘└─┘└─
260 rw [← int.mul_div_cancel (term.val _ _) h3, ← h4, int.zero_div]
id └────────────────┘ └──────┘ └┘ └┘ └──────────┘
src └────┘└────────────────┘┴ └──────┘└────┘ └──┘ └┘└──────────┘└┘
typ └────┘└────────────────┘┴ └──────┘└────┘└┘└──┘└┘└┘└──────────┘└┘
doc └────┘ ┴ └────┘ └──┘ └┘ └┘
txt └────┘ ┴ └────┘ └──┘ └┘ └┘
par └────┘ ┴ └────┘ └──┘ └┘ └┘
pid └──┘ ┴ └────┘ └──┘ └┘ ┴┴
st ───────────────────────────────────────────┘└────┘└────────────┘┴┴
261 end
st └─┘
262
263 -- Requires : t1.coeffs[m] = 1
264 def cancel (m : nat) (t1 t2 : term) : term :=
id └─┘ └──┘ └──┘
src └─┘ └──┘ └──┘
typ └─┘ └──┘ └──┘
265 term.add (t1.mul (-(get m (t2.snd)))) t2
id └──────┘ └┘└──┘ ┴ └─┘ ┴ └┘└──┘ └┘
src └──────┘ └──┘ ┴ └─┘ └──┘
typ └──────┘ └┘└──┘ ┴ └─┘ ┴ └┘└──┘ └┘
266
267 def subst (n : nat) (t1 t2 : term) : term :=
id └─┘ └──┘ └──┘
src └─┘ └──┘ └──┘
typ └─┘ └──┘ └──┘
268 term.add (t1.mul (get n t2.snd)) (t2.fst, t2.snd {n ↦ 0})
id └──────┘ └┘└──┘ └─┘ ┴ └┘└──┘ ┴└┘└──┘ └┘└──┘ ┴┴ ┴ ┴
src └──────┘ └──┘ └─┘ └──┘ ┴ └──┘ └──┘ ┴ ┴ ┴
typ └──────┘ └┘└──┘ └─┘ ┴ └┘└──┘ ┴└┘└──┘ └┘└──┘ ┴┴ ┴ ┴
269
270 lemma subst_correct {v : nat → int} {b : int}
id └─┘ └─┘ └─┘
src └─┘ └─┘ └─┘
typ └─┘ └─┘ └─┘
271 {as : list int} {t : term} {n : nat} :
id └──┘ └─┘ └──┘ └─┘
src └──┘ └─┘ └──┘ └─┘
typ └──┘ └─┘ └──┘ └─┘
272 0 < get n as → 0 = term.val v (b,as) →
id ┴ └─┘ ┴ └┘ ┴ └──────┘ ┴ ┴┴ └┘
src ┴ └─┘ ┴ └──────┘ ┴
typ ┴ └─┘ ┴ └┘ ┴ └──────┘ ┴ ┴┴ └┘
273 term.val v t = term.val (v ⟨n ↦ sgm v b as n⟩) (subst n (rhs n b as) t) :=
id └──────┘ ┴ ┴ ┴ └──────┘ ┴ ┴┴ ┴ └─┘ ┴ ┴ └┘ ┴┴ └───┘ ┴ └─┘ ┴ ┴ └┘ ┴
src └──────┘ ┴ └──────┘ ┴ ┴ └─┘ ┴ └───┘ └─┘
typ └──────┘ ┴ ┴ ┴ └──────┘ ┴ ┴┴ ┴ └─┘ ┴ ┴ └┘ ┴┴ └───┘ ┴ └─┘ ┴ ┴ └┘ ┴
274 begin
st └─────
275 intros h1 h2,
src └──────────┘
typ └──────────┘
doc └──────────┘
txt └──────────┘
par └──────────┘
pid └────┘
st ─────────────┘└─
276 simp only [subst, term.val, term.val_add, term.val_mul],
id └───┘ └──────┘ └──────────┘ └──────────┘
src └─────────┘└───┘└┘└──────┘└┘└──────────┘└┘└──────────┘┴
typ └─────────┘└───┘└┘└──────┘└┘└──────────┘└┘└──────────┘┴
doc └─────────┘ └┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ └┘ ┴
st ────────────────────────────────────────────────────────┘└─
277 rw ← rhs_correct _ h1 h2,
id └─────────┘ └┘ └┘
src └───┘└─────────┘└─┘ ┴
typ └───┘└─────────┘└─┘└┘┴└┘
doc └───┘ └─┘ ┴
txt └───┘ └─┘ ┴
par └───┘ └─┘ ┴
pid └─┘ └─┘ ┴
st ─────────────────────────┘└─
278 cases t with b' as',
id ┴
src └────┘ └──────────┘
typ └────┘┴└──────────┘
doc └────┘ └──────────┘
txt └────┘ └──────────┘
par └────┘ └──────────┘
pid ┴ └──────────┘
st ────────────────────┘└─
279 simp only [term.val],
id └──────┘
src └─────────┘└──────┘┴
typ └─────────┘└──────┘┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st ─────────────────────┘└─
280 have h3 : coeffs.val (v ⟨n ↦ sgm v b as n⟩) (as' {n ↦ 0}) =
id └────────┘ └─┘ ┴ └┘ ┴ ┴ ┴ ┴
src └────────┘└────────┘┴ ┴ ┴ ┴└─┘┴ ┴ ┴ ┴ └┘ ┴┴ ┴┴└┘┴└┘┴└
typ └────────┘└────────┘┴ ┴ ┴ ┴└─┘┴ ┴┴┴└┘┴ └┘ ┴┴ ┴┴└┘┴└┘┴└
doc └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ └┘ └
txt └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ └┘ └
par └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ └┘ └
pid └─────┘└─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ └┘ └
st ──────────────────────────────────────────────────────────────
281 coeffs.val_except n v as',
id └───────────────┘ ┴ ┴ └─┘
src ───┘└───────────────┘┴ ┴ ┴
typ ───┘└───────────────┘┴┴┴┴┴└─┘
doc ───┘ ┴ ┴ ┴
txt ───┘ ┴ ┴ ┴
par ───┘ ┴ ┴ ┴
pid ───┘ ┴ ┴ ┴
st ────────────────────────────┘└─
282 { rw [← coeffs.val_except_add_eq n, get_set,
id └──────────────────────┘ ┴ └─────┘
src └────┘└──────────────────────┘┴ └┘└─────┘└─
typ └────┘└──────────────────────┘┴┴└┘└─────┘└─
doc └────┘ ┴ └┘ └─
txt └────┘ ┴ └┘ └─
par └────┘ ┴ └┘ └─
pid └──┘ ┴ └┘ └─
st ───┘└──────────────────────────────┘└───────┘└─
283 zero_mul, add_zero, coeffs.val_except_update_set] },
id └──────┘ └──────┘ └──────────────────────────┘
src ─────┘└──────┘└┘└──────┘└┘└──────────────────────────┘└┘
typ ─────┘└──────┘└┘└──────┘└┘└──────────────────────────┘└┘
doc ─────┘ └┘ └┘ └┘
txt ─────┘ └┘ └┘ └┘
par ─────┘ └┘ └┘ └┘
pid ─────┘ └┘ └┘ ┴┴
st ─────────────┘└────────┘└────────────────────────────┘┴┴└┘└
284 rw [h3, ← coeffs.val_except_add_eq n], ring
id └┘ └──────────────────────┘ ┴
src └──┘ └──┘└──────────────────────┘┴ ┴ └───┘
typ └──┘└┘└──┘└──────────────────────┘┴┴┴ └───┘
doc └──┘ └──┘ ┴ ┴ └───┘
txt └──┘ └──┘ ┴ ┴ └───┘
par └──┘ └──┘ ┴ ┴ └───┘
pid └┘ └──┘ ┴ ┴ ┴
st ───────┘└────────────────────────────┘└──────┘
285 end
st └─┘
286
287 /- The type of equality elimination rules. -/
288
289 @[derive has_reflect, derive inhabited]
id └─────────┘ └───────┘
src └─────────┘ └───────┘
typ └─────────┘ └───────┘
doc └────┘ └────┘
290 inductive ee : Type
291 | drop : ee
292 | nondiv : int → ee
id └─┘
src └─┘
typ └─┘
293 | factor : int → ee
id └─┘
src └─┘
typ └─┘
294 | neg : ee
295 | reduce : nat → ee
id └─┘
src └─┘
typ └─┘
296 | cancel : nat → ee
id └─┘
src └─┘
typ └─┘
297
298 namespace ee
299
300 def repr : ee → string
id └┘ ┴ └────┘
src └┘ ┴ └────┘
typ └┘ ┴ └────┘
301 | drop := "↓"
id └──┘
src └──┘
typ └──┘
302 | (nondiv i) := i.repr ++ "∤"
id └────┘ ┴ └───┘ └┘
src └────┘ └───┘ └┘
typ └────┘ ┴ └───┘ └┘
303 | (factor i) := "/" ++ i.repr
id └────┘ ┴ └┘ └───┘
src └────┘ └┘ └───┘
typ └────┘ ┴ └┘ └───┘
304 | neg := "-"
id └─┘
src └─┘
typ └─┘
305 | (reduce n) := "≻" ++ n.repr
id └────┘ ┴ └┘ └───┘
src └────┘ └┘ └───┘
typ └────┘ ┴ └┘ └───┘
306 | (cancel n) := "+" ++ n.repr
id └────┘ ┴ └┘ └───┘
src └────┘ └┘ └───┘
typ └────┘ ┴ └┘ └───┘
307
308 instance has_repr : has_repr ee := ⟨repr⟩
id └──────┘ └┘ └──┘
src └──────┘ └┘ └──┘
typ └──────┘ └┘ └──┘
309
310 meta instance has_to_format : has_to_format ee := ⟨λ x, x.repr⟩
id └───────────┘ └┘ ┴ ┴└───┘
src └───────────┘ └┘ └───┘
typ └───────────┘ └┘ ┴ ┴└───┘
311
312 end ee
313
314 def eq_elim : list ee → clause → clause
id └──┘ └┘ ┴ └────┘ └────┘
src └──┘ └┘ └────┘ └────┘
typ └──┘ └┘ ┴ └────┘ └────┘
315 | [] ([], les) := ([],les)
id └┘ ┴└┘ └─┘ ┴└┘
src └┘ ┴└┘ ┴└┘
typ └┘ ┴└┘ └─┘ ┴└┘
316 | [] ((_::_), les) := ([],[])
id └┘ ┴ └┘ ┴└┘ └┘
src └┘ ┴ └┘ ┴└┘ └┘
typ └┘ ┴ └┘ ┴└┘ └┘
317 | (_::_) ([], les) := ([],[])
id └┘ ┴└┘ ┴└┘ └┘
src └┘ ┴└┘ ┴└┘ └┘
typ └┘ ┴└┘ ┴└┘ └┘
318 | (ee.drop::es) ((eq::eqs), les) := eq_elim es (eqs, les)
id └─────┘└┘└┘ ┴ └┘└─┘ └─┘ └─────┘ ┴
src └─────┘└┘ ┴ └┘ ┴
typ └─────┘└┘└┘ ┴ └┘└─┘ └─┘ └─────┘ ┴
319 | (ee.neg::es) ((eq::eqs), les) := eq_elim es ((eq.neg::eqs), les)
id └────┘└┘└┘ ┴ └┘└┘└─┘ └─┘ └─────┘ ┴ └──┘└┘
src └────┘└┘ ┴ └┘└┘ ┴ └──┘└┘
typ └────┘└┘└┘ ┴ └┘└┘└─┘ └─┘ └─────┘ ┴ └──┘└┘
320 | (ee.nondiv i::es) ((b,as)::eqs, les) :=
id └───────┘ ┴└┘ └┘┴ └┘ └┘
src └───────┘ └┘ └┘ └┘
typ └───────┘ ┴└┘ └┘┴ └┘ └┘
321 if ¬(i ∣ b) ∧ (∀ x ∈ as, i ∣ x)
id ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
322 then ([],[⟨-1,[]⟩])
id ┴└┘ ┴ ┴ └┘ ┴
src ┴└┘ ┴ ┴ └┘ ┴
typ ┴└┘ ┴ ┴ └┘ ┴
323 else ([],[])
id ┴└┘ └┘
src ┴└┘ └┘
typ ┴└┘ └┘
324 | (ee.factor i::es) ((b,as)::eqs, les) :=
id └───────┘ ┴└┘└┘ └┘┴ └┘ └┘└─┘ └─┘
src └───────┘ └┘ └┘ └┘
typ └───────┘ ┴└┘└┘ └┘┴ └┘ └┘└─┘ └─┘
325 if (i ∣ b) ∧ (∀ x ∈ as, i ∣ x)
id ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
326 then eq_elim es ((term.div i (b,as)::eqs), les)
id └─────┘ ┴ └──────┘ ┴ └┘
src ┴ └──────┘ ┴ └┘
typ └─────┘ ┴ └──────┘ ┴ └┘
327 else ([],[])
id ┴└┘ └┘
src ┴└┘ └┘
typ ┴└┘ └┘
328 | (ee.reduce n::es) ((b,as)::eqs, les) :=
id └───────┘ ┴└┘└┘ └┘┴ └┘ └┘└─┘ └─┘
src └───────┘ └┘ └┘ └┘
typ └───────┘ ┴└┘└┘ └┘┴ └┘ └┘└─┘ └─┘
329 if 0 < get n as
id ┴ └─┘
src ┴ └─┘
typ ┴ └─┘
330 then let eq' := coeffs_reduce n b as in
id └─┘ └───────────┘
src └───────────┘
typ └─┘ └───────────┘
331 let r := rhs n b as in
id ┴ └─┘
src └─┘
typ ┴ └─┘
332 let eqs' := eqs.map (subst n r) in
id └──┘ └──┘ └───┘ ┴
src └──┘ └───┘
typ └──┘ └──┘ └───┘ ┴
333 let les' := les.map (subst n r) in
id └──┘ └──┘ └───┘ ┴
src └──┘ └───┘
typ └──┘ └──┘ └───┘ ┴
334 eq_elim es ((eq'::eqs'), les')
id └─────┘ ┴ └─┘└┘└──┘ └──┘
src ┴ └┘
typ └─────┘ ┴ └─┘└┘└──┘ └──┘
335 else ([],[])
id ┴└┘ └┘
src ┴└┘ └┘
typ ┴└┘ └┘
336 | (ee.cancel m::es) ((eq::eqs), les) :=
id └───────┘ ┴└┘└┘ ┴ └┘└┘└─┘ └─┘
src └───────┘ └┘ ┴ └┘└┘
typ └───────┘ ┴└┘└┘ ┴ └┘└┘└─┘ └─┘
337 eq_elim es ((eqs.map (cancel m eq)), (les.map (cancel m eq)))
id └─────┘ ┴ └──┘ └────┘ └──┘ └────┘
src ┴ └──┘ └────┘ └──┘ └────┘
typ └─────┘ ┴ └──┘ └────┘ └──┘ └────┘
338
339 open tactic
340
341 lemma sat_empty : clause.sat ([],[]) :=
id └────────┘ ┴└┘ └┘
src └────────┘ ┴└┘ └┘
typ └────────┘ ┴└┘ └┘
342 ⟨λ _,0, ⟨dec_trivial, dec_trivial⟩⟩
id ┴ └─────────┘ └─────────┘
src └─────────┘ └─────────┘
typ ┴ └─────────┘ └─────────┘
doc └─────────┘ └─────────┘
343
344 lemma sat_eq_elim :
345 ∀ {es : list ee} {c : clause}, c.sat → (eq_elim es c).sat
id ┴ └──┘ └┘ └────┘ ┴└──┘ └─────┘ └┘ ┴ └─┘
src └──┘ └┘ └────┘ └──┘ └─────┘ └─┘
typ ┴ └──┘ └┘ └────┘ ┴└──┘ └─────┘ └┘ ┴ └─┘
346 | [] ([], les) h := h
id └┘ ┴└┘ ┴
src └┘ ┴└┘
typ └┘ ┴└┘ ┴
347 | (e::_) ([], les) h :=
id └┘ ┴└┘
src └┘ ┴└┘
typ └┘ ┴└┘
348 by {cases e; simp only [eq_elim]; apply sat_empty}
id ┴ └─────┘ └───────┘
src └────┘ └─────────┘└─────┘┴ └────┘└───────┘
typ └────┘┴ └─────────┘└─────┘┴ └────┘└───────┘
doc └────┘ └─────────┘ ┴ └────┘
txt └────┘ └─────────┘ ┴ └────┘
par └────┘ └─────────┘ ┴ └────┘
pid ┴ ┴└──┘└┘ ┴ ┴
st └─────────────────────────────────────────────┘└┘
349 | [] ((_::_), les) h := sat_empty
id └┘ ┴ └┘ └───────┘
src └┘ ┴ └┘ └───────┘
typ └┘ ┴ └┘ └───────┘
350 | (ee.drop::es) ((eq::eqs), les) h1 :=
id └─────┘└┘ ┴ └┘
src └─────┘└┘ ┴ └┘
typ └─────┘└┘ ┴ └┘
351 begin
st └─────
352 apply (@sat_eq_elim es _ _),
id └─────────┘ └┘
src └────┘ ┴ └───┘
typ └────┘ └─────────┘┴└┘└───┘
doc └────┘ ┴ └───┘
txt └────┘ ┴ └───┘
par └────┘ ┴ └───┘
pid ┴ ┴ └───┘
st ──────────────────────────────┘└─
353 rcases h1 with ⟨v,h1,h2⟩,
id └┘
src └─────┘ └─────────────┘
typ └─────┘└┘└─────────────┘
doc └─────┘ └─────────────┘
txt └─────┘ └─────────────┘
par └─────┘ └─────────────┘
pid ┴ └─────────────┘
st ───────────────────────────┘└─
354 refine ⟨v, list.forall_mem_of_forall_mem_cons h1, h2⟩
id ┴ └────────────────────────────────┘ └┘ └┘
src └─────┘ └┘└────────────────────────────────┘┴ └┘ └─
typ └─────┘ ┴└┘└────────────────────────────────┘┴└┘└┘└┘└─
doc └─────┘ └┘ ┴ └┘ └─
txt └─────┘ └┘ ┴ └┘ └─
par └─────┘ └┘ ┴ └┘ └─
pid ┴ └┘ ┴ └┘ ┴└
st ──────────────────────────────────────────────────────────
355 end
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
356 | (ee.neg::es) ((eq::eqs), les) h1 :=
id └────┘└┘ ┴ └┘
src └────┘└┘ ┴ └┘
typ └────┘└┘ ┴ └┘
357 begin
st └─────
358 simp only [eq_elim], apply sat_eq_elim,
id └─────┘
src └─────────┘└─────┘┴ └────┘
typ └─────────┘└─────┘┴ └────┘
doc └─────────┘ ┴ └────┘
txt └─────────┘ ┴ └────┘
par └─────────┘ ┴ └────┘
pid ┴└──┘└┘ ┴ ┴
st ──────────────────────┘└─────────────────┘└─
359 cases h1 with v h1,
id └┘
src └────┘ └────────┘
typ └────┘└┘└────────┘
doc └────┘ └────────┘
txt └────┘ └────────┘
par └────┘ └────────┘
pid ┴ └────────┘
st ─────────────────────┘└─
360 existsi v,
id ┴
src └──────┘
typ └──────┘┴
doc └──────┘
txt └──────┘
par └──────┘
pid ┴
st ────────────┘└─
361 cases h1 with hl hr,
id └┘
src └────┘ └─────────┘
typ └────┘└┘└─────────┘
doc └────┘ └─────────┘
txt └────┘ └─────────┘
par └────┘ └─────────┘
pid ┴ └─────────┘
st ──────────────────────┘└─
362 apply and.intro _ hr,
id └───────┘ └┘
src └────┘└───────┘└─┘
typ └────┘└───────┘└─┘└┘
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └─┘
st ───────────────────────┘└─
363 rw list.forall_mem_cons at *,
id └──────────────────┘
src └─┘└──────────────────┘└───┘
typ └─┘└──────────────────┘└───┘
doc └─┘ └───┘
txt └─┘ └───┘
par └─┘ └───┘
pid ┴ └───┘
st ───────────────────────────────┘└─
364 apply and.intro _ hl.right,
id └───────┘ └──────┘
src └────┘└───────┘└─┘└──────┘
typ └────┘└───────┘└─┘└──────┘
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └─┘
st ─────────────────────────────┘└─
365 rw term.val_neg,
id └──────────┘
src └─┘└──────────┘
typ └─┘└──────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ──────────────────┘└─
366 rw ← hl.left,
src └───┘
typ └───┘└─────┘
doc └───┘
txt └───┘
par └───┘
pid └─┘
st ───────────────┘└─
367 refl
src └────
typ └────
doc └────
txt └────
par └────
pid └
st ─────────
368 end
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
369 | (ee.nondiv i::es) ((b,as)::eqs, les) h1 :=
id └───────┘ └┘ └┘ └┘
src └───────┘ └┘ └┘ └┘
typ └───────┘ └┘ └┘ └┘
370 begin
st └─────
371 unfold eq_elim,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid └──────┘
st ─────────────────┘└─
372 by_cases h2 : (¬i ∣ b ∧ ∀ (x : ℤ), x ∈ as → i ∣ x),
id ┴ ┴ ┴ └┘ ┴
src └───────┘ └─┘ ┴┴┴ ┴ ┴ └────┘ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴
typ └───────┘ └─┘ ┴┴┴┴┴ ┴ └────┘ ┴ ┴ ┴┴┴└┘┴ ┴┴┴ ┴ ┴
doc └───────┘ └─┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
txt └───────┘ └─┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └───────┘ └─┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid ┴ └─┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ─────────────────────────────────────────────────────┘└─
373 { exfalso, cases h1 with v h1,
id └┘
src └─────┘ └────┘ └────────┘
typ └─────┘ └────┘└┘└────────┘
doc └─────┘ └────┘ └────────┘
txt └─────┘ └────┘ └────────┘
par └─────┘ └────┘ └────────┘
pid ┴ └────────┘
st ─────┘└─────┘└──────────────────┘└─
374 have h3 : 0 = b + coeffs.val v as := h1.left _ (or.inl rfl),
id ┴ ┴ ┴ └────────┘ ┴ └┘ └─────┘ └────┘ └─┘
src └──────────┘┴┴ ┴┴┴└────────┘┴ ┴ └──┘└─────┘└─┘ └────┘┴└─┘┴
typ └──────────┘┴┴┴┴┴┴└────────┘┴┴┴└┘└──┘└─────┘└─┘ └────┘┴└─┘┴
doc └──────────┘ ┴ ┴ ┴ ┴ ┴ └──┘ └─┘ ┴ ┴
txt └──────────┘ ┴ ┴ ┴ ┴ ┴ └──┘ └─┘ ┴ ┴
par └──────────┘ ┴ ┴ ┴ ┴ ┴ └──┘ └─┘ ┴ ┴
pid └─────┘└───┘ ┴ ┴ ┴ ┴ ┴ └──┘ └─┘ ┴ ┴
st ────────────────────────────────────────────────────────────────┘└─
375 have h4 : i ∣ coeffs.val v as := coeffs.dvd_val h2.right,
id ┴ └────────┘ ┴ └┘ └────────────┘ └──────┘
src └────────┘ ┴ ┴└────────┘┴ ┴ └──────┘└────────────┘┴└──────┘
typ └────────┘┴┴ ┴└────────┘┴┴┴└┘└──────┘└────────────┘┴└──────┘
doc └────────┘ ┴ ┴ ┴ ┴ └──────┘ ┴
txt └────────┘ ┴ ┴ ┴ ┴ └──────┘ ┴
par └────────┘ ┴ ┴ ┴ ┴ └──────┘ ┴
pid └─────┘└─┘ ┴ ┴ ┴ ┴ └──────┘ ┴
st ─────────────────────────────────────────────────────────────────┘└─
376 have h5 : i ∣ b + coeffs.val v as := by { rw ← h3, apply dvd_zero },
id ┴ ┴ └────────┘ ┴ └┘ └┘ └──────┘
src └────────┘ ┴ ┴ ┴ ┴└────────┘┴ ┴ └──┘ └─┘└───┘ └┘└────┘└──────┘┴┴
typ └────────┘┴┴ ┴┴┴ ┴└────────┘┴┴┴└┘└──┘ └─┘└───┘└┘└┘└────┘└──────┘┴┴
doc └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └─┘└───┘ └┘└────┘ ┴┴
txt └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └─┘└───┘ └┘└────┘ ┴┴
par └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └─┘└───┘ └┘└────┘ ┴┴
pid └─────┘└─┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └──────┘ └──────┘ └┘
st ────────────────────────────────────────────┘└────────┘└───────────────┘└┘└
377 rw ← dvd_add_iff_left h4 at h5, apply h2.left h5 },
id └──────────────┘ └┘ └─────┘ └┘
src └───┘└──────────────┘┴ └────┘ └────┘└─────┘┴ ┴
typ └───┘└──────────────┘┴└┘└────┘ └────┘└─────┘┴└┘┴
doc └───┘ ┴ └────┘ └────┘ ┴ ┴
txt └───┘ ┴ └────┘ └────┘ ┴ ┴
par └───┘ ┴ └────┘ └────┘ ┴ ┴
pid └─┘ ┴ └────┘ ┴ ┴ ┴
st ───────────────────────────────────┘└─────────────────┘└┘└
378 rw if_neg h2, apply sat_empty
id └────┘ └┘ └───────┘
src └─┘└────┘┴ └────┘└───────┘└
typ └─┘└────┘┴└┘ └────┘└───────┘└
doc └─┘ ┴ └────┘ └
txt └─┘ ┴ └────┘ └
par └─┘ ┴ └────┘ └
pid ┴ ┴ ┴ └
st ───────────────┘└─────────────────
379 end
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
380 | (ee.factor i::es) ((b,as)::eqs, les) h1 :=
id └───────┘ └┘ └┘ └┘
src └───────┘ └┘ └┘ └┘
typ └───────┘ └┘ └┘ └┘
381 begin
st └─────
382 simp only [eq_elim],
id └─────┘
src └─────────┘└─────┘┴
typ └─────────┘└─────┘┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st ──────────────────────┘└─
383 by_cases h2 : (i ∣ b) ∧ (∀ x ∈ as, i ∣ x),
id ┴ └┘ ┴
src └───────┘ └─┘ ┴ ┴ └┘ ┴ └───┘ ┴ ┴ ┴ ┴
typ └───────┘ └─┘ ┴ ┴┴└┘ ┴ └───┘└┘ ┴┴┴ ┴ ┴
doc └───────┘ └─┘ ┴ ┴ └┘ ┴ └───┘ ┴ ┴ ┴ ┴
txt └───────┘ └─┘ ┴ ┴ └┘ ┴ └───┘ ┴ ┴ ┴ ┴
par └───────┘ └─┘ ┴ ┴ └┘ ┴ └───┘ ┴ ┴ ┴ ┴
pid ┴ └─┘ ┴ ┴ └┘ ┴ └───┘ ┴ ┴ ┴ ┴
st ────────────────────────────────────────────┘└─
384 { rw if_pos h2, apply sat_eq_elim, cases h1 with v h1,
id └────┘ └┘ └┘
src └─┘└────┘┴ └────┘ └────┘ └────────┘
typ └─┘└────┘┴└┘ └────┘ └────┘└┘└────────┘
doc └─┘ ┴ └────┘ └────┘ └────────┘
txt └─┘ ┴ └────┘ └────┘ └────────┘
par └─┘ ┴ └────┘ └────┘ └────────┘
pid ┴ ┴ ┴ ┴ └────────┘
st ─────┘└──────────┘└─────────────────┘└──────────────────┘└─
385 existsi v, cases h1 with h3 h4, apply and.intro _ h4,
id ┴ └┘ └───────┘ └┘
src └──────┘ └────┘ └─────────┘ └────┘└───────┘└─┘
typ └──────┘┴ └────┘└┘└─────────┘ └────┘└───────┘└─┘└┘
doc └──────┘ └────┘ └─────────┘ └────┘ └─┘
txt └──────┘ └────┘ └─────────┘ └────┘ └─┘
par └──────┘ └────┘ └─────────┘ └────┘ └─┘
pid ┴ ┴ └─────────┘ ┴ └─┘
st ──────────────┘└───────────────────┘└────────────────────┘└─
386 rw list.forall_mem_cons at *, cases h3 with h5 h6,
id └──────────────────┘ └┘
src └─┘└──────────────────┘└───┘ └────┘ └─────────┘
typ └─┘└──────────────────┘└───┘ └────┘└┘└─────────┘
doc └─┘ └───┘ └────┘ └─────────┘
txt └─┘ └───┘ └────┘ └─────────┘
par └─┘ └───┘ └────┘ └─────────┘
pid ┴ └───┘ ┴ └─────────┘
st ─────────────────────────────────┘└───────────────────┘└─
387 apply and.intro _ h6,
id └───────┘ └┘
src └────┘└───────┘└─┘
typ └────┘└───────┘└─┘└┘
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └─┘
st ─────────────────────────┘└─
388 rw [term.val_div h2.left h2.right, ← h5, int.zero_div] },
id └──────────┘ └─────┘ └──────┘ └┘ └──────────┘
src └──┘└──────────┘┴└─────┘┴└──────┘└──┘ └┘└──────────┘└┘
typ └──┘└──────────┘┴└─────┘┴└──────┘└──┘└┘└┘└──────────┘└┘
doc └──┘ ┴ ┴ └──┘ └┘ └┘
txt └──┘ ┴ ┴ └──┘ └┘ └┘
par └──┘ ┴ ┴ └──┘ └┘ └┘
pid └┘ ┴ ┴ └──┘ └┘ ┴┴
st ──────────────────────────────────────┘└────┘└────────────┘┴┴└┘└
389 { rw if_neg h2, apply sat_empty }
id └────┘ └┘ └───────┘
src └─┘└────┘┴ └────┘└───────┘┴
typ └─┘└────┘┴└┘ └────┘└───────┘┴
doc └─┘ ┴ └────┘ ┴
txt └─┘ ┴ └────┘ ┴
par └─┘ ┴ └────┘ ┴
pid ┴ ┴ ┴ ┴
st ─────────────────┘└────────────────┘└─
390 end
st ────┘
391 | (ee.reduce n::es) ((b,as)::eqs, les) h1 :=
id └───────┘ └┘ └┘ └┘
src └───────┘ └┘ └┘ └┘
typ └───────┘ └┘ └┘ └┘
392 begin
st └─────
393 simp only [eq_elim],
id └─────┘
src └─────────┘└─────┘┴
typ └─────────┘└─────┘┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st ──────────────────────┘└─
394 by_cases h2 : 0 < get n as,
id ┴ └─┘ ┴ └┘
src └───────┘ └───┘┴┴└─┘┴ ┴
typ └───────┘ └───┘┴┴└─┘┴┴┴└┘
doc └───────┘ └───┘ ┴ ┴ ┴
txt └───────┘ └───┘ ┴ ┴ ┴
par └───────┘ └───┘ ┴ ┴ ┴
pid ┴ └───┘ ┴ ┴ ┴
st ─────────────────────────────┘└─
395 tactic.rotate 1,
id └───────────┘
src └───────────┘
typ └───────────┘
par └───────────┘
st ─────────────────┘└──
396 { rw if_neg h2, apply sat_empty },
id └────┘ └┘ └───────┘
src └─┘└────┘┴ └────┘└───────┘┴
typ └─┘└────┘┴└┘ └────┘└───────┘┴
doc └─┘ ┴ └────┘ ┴
txt └─┘ ┴ └────┘ ┴
par └─┘ ┴ └────┘ ┴
pid ┴ ┴ ┴ ┴
st ─────┘└──────────┘└────────────────┘└┘└
397 rw if_pos h2,
id └────┘ └┘
src └─┘└────┘┴
typ └─┘└────┘┴└┘
doc └─┘ ┴
txt └─┘ ┴
par └─┘ ┴
pid ┴ ┴
st ───────────────┘└─
398 apply sat_eq_elim,
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ────────────────────┘└─
399 cases h1 with v h1,
id └┘
src └────┘ └────────┘
typ └────┘└┘└────────┘
doc └────┘ └────────┘
txt └────┘ └────────┘
par └────┘ └────────┘
pid ┴ └────────┘
st ─────────────────────┘└─
400 existsi v ⟨n ↦ sgm v b as n⟩,
id ┴ ┴ ┴ └─┘ ┴ └┘ ┴┴
src └──────┘ ┴┴ ┴┴┴└─┘┴ ┴ ┴ ┴ ┴
typ └──────┘┴┴┴ ┴┴┴└─┘┴ ┴┴┴└┘┴┴┴
doc └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
txt └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ───────────────────────────────┘└─
401 cases h1 with h1 h3,
id └┘
src └────┘ └─────────┘
typ └────┘└┘└─────────┘
doc └────┘ └─────────┘
txt └────┘ └─────────┘
par └────┘ └─────────┘
pid ┴ └─────────┘
st ──────────────────────┘└─
402 rw list.forall_mem_cons at h1,
id └──────────────────┘
src └─┘└──────────────────┘└────┘
typ └─┘└──────────────────┘└────┘
doc └─┘ └────┘
txt └─┘ └────┘
par └─┘ └────┘
pid ┴ └────┘
st ────────────────────────────────┘└─
403 cases h1 with h4 h5,
id └┘
src └────┘ └─────────┘
typ └────┘└┘└─────────┘
doc └────┘ └─────────┘
txt └────┘ └─────────┘
par └────┘ └─────────┘
pid ┴ └─────────┘
st ──────────────────────┘└─
404 constructor,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
st ──────────────┘└─
405 { rw list.forall_mem_cons,
id └──────────────────┘
src └─┘└──────────────────┘
typ └─┘└──────────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ─────┘└─────────────────────┘└─
406 constructor,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
st ────────────────┘└─
407 { apply coeffs_reduce_correct h2 h4 },
id └───────────────────┘ └┘ └┘
src └────┘└───────────────────┘┴ ┴ ┴
typ └────┘└───────────────────┘┴└┘┴└┘┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ───────┘└────────────────────────────────┘└┘└
408 { intros x h6, rw list.mem_map at h6,
id └──────────┘
src └─────────┘ └─┘└──────────┘└────┘
typ └─────────┘ └─┘└──────────┘└────┘
doc └─────────┘ └─┘ └────┘
txt └─────────┘ └─┘ └────┘
par └─────────┘ └─┘ └────┘
pid └───┘ ┴ └────┘
st ──────────────────┘└─────────────────────┘└─
409 cases h6 with t h6, cases h6 with h6 h7,
id └┘ └┘
src └────┘ └────────┘ └────┘ └─────────┘
typ └────┘└┘└────────┘ └────┘└┘└─────────┘
doc └────┘ └────────┘ └────┘ └─────────┘
txt └────┘ └────────┘ └────┘ └─────────┘
par └────┘ └────────┘ └────┘ └─────────┘
pid ┴ └────────┘ ┴ └─────────┘
st ─────────────────────────┘└───────────────────┘└─
410 rw [← h7, ← subst_correct h2 h4], apply h5 _ h6 } },
id └┘ └───────────┘ └┘ └┘ └┘ └┘
src └────┘ └──┘└───────────┘┴ ┴ ┴ └────┘ └─┘ ┴
typ └────┘└┘└──┘└───────────┘┴└┘┴└┘┴ └────┘└┘└─┘└┘┴
doc └────┘ └──┘ ┴ ┴ ┴ └────┘ └─┘ ┴
txt └────┘ └──┘ ┴ ┴ ┴ └────┘ └─┘ ┴
par └────┘ └──┘ ┴ ┴ ┴ └────┘ └─┘ ┴
pid └──┘ └──┘ ┴ ┴ ┴ ┴ └─┘ ┴
st ───────────────┘└─────────────────────┘└───────────────┘└──┘└
411 { intros x h6, rw list.mem_map at h6,
id └──────────┘
src └─────────┘ └─┘└──────────┘└────┘
typ └─────────┘ └─┘└──────────┘└────┘
doc └─────────┘ └─┘ └────┘
txt └─────────┘ └─┘ └────┘
par └─────────┘ └─┘ └────┘
pid └───┘ ┴ └────┘
st ────────────────┘└─────────────────────┘└─
412 cases h6 with t h6, cases h6 with h6 h7,
id └┘ └┘
src └────┘ └────────┘ └────┘ └─────────┘
typ └────┘└┘└────────┘ └────┘└┘└─────────┘
doc └────┘ └────────┘ └────┘ └─────────┘
txt └────┘ └────────┘ └────┘ └─────────┘
par └────┘ └────────┘ └────┘ └─────────┘
pid ┴ └────────┘ ┴ └─────────┘
st ───────────────────────┘└───────────────────┘└─
413 rw [← h7, ← subst_correct h2 h4], apply h3 _ h6 }
id └┘ └───────────┘ └┘ └┘ └┘ └┘
src └────┘ └──┘└───────────┘┴ ┴ ┴ └────┘ └─┘ ┴
typ └────┘└┘└──┘└───────────┘┴└┘┴└┘┴ └────┘└┘└─┘└┘┴
doc └────┘ └──┘ ┴ ┴ ┴ └────┘ └─┘ ┴
txt └────┘ └──┘ ┴ ┴ ┴ └────┘ └─┘ ┴
par └────┘ └──┘ ┴ ┴ ┴ └────┘ └─┘ ┴
pid └──┘ └──┘ ┴ ┴ ┴ ┴ └─┘ ┴
st ─────────────┘└─────────────────────┘└───────────────┘└─
414 end
st ─────┘
415 | (ee.cancel m::es) ((eq::eqs), les) h1 :=
id └───────┘ └┘ ┴ └┘
src └───────┘ └┘ ┴ └┘
typ └───────┘ └┘ ┴ └┘
416 begin
st └─────
417 unfold eq_elim,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid └──────┘
st ─────────────────┘└─
418 apply sat_eq_elim,
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ────────────────────┘└─
419 cases h1 with v h1,
id └┘
src └────┘ └────────┘
typ └────┘└┘└────────┘
doc └────┘ └────────┘
txt └────┘ └────────┘
par └────┘ └────────┘
pid ┴ └────────┘
st ─────────────────────┘└─
420 existsi v,
id ┴
src └──────┘
typ └──────┘┴
doc └──────┘
txt └──────┘
par └──────┘
pid ┴
st ────────────┘└─
421 cases h1 with h1 h2,
id └┘
src └────┘ └─────────┘
typ └────┘└┘└─────────┘
doc └────┘ └─────────┘
txt └────┘ └─────────┘
par └────┘ └─────────┘
pid ┴ └─────────┘
st ──────────────────────┘└─
422 rw list.forall_mem_cons at h1, cases h1 with h1 h3,
id └──────────────────┘ └┘
src └─┘└──────────────────┘└────┘ └────┘ └─────────┘
typ └─┘└──────────────────┘└────┘ └────┘└┘└─────────┘
doc └─┘ └────┘ └────┘ └─────────┘
txt └─┘ └────┘ └────┘ └─────────┘
par └─┘ └────┘ └────┘ └─────────┘
pid ┴ └────┘ ┴ └─────────┘
st ────────────────────────────────┘└───────────────────┘└─
423 constructor; intros t h4; rw list.mem_map at h4;
id └──────────┘
src └─────────┘ └─────────┘ └─┘└──────────┘└────┘
typ └─────────┘ └─────────┘ └─┘└──────────┘└────┘
doc └─────────┘ └─────────┘ └─┘ └────┘
txt └─────────┘ └─────────┘ └─┘ └────┘
par └─────────┘ └─────────┘ └─┘ └────┘
pid └───┘ ┴ └────┘
st ────────────────────────────────┘└──────────┘└───────
424 rcases h4 with ⟨s,h4,h5⟩; rw ← h5;
id └┘ └┘
src └─────┘ └─────────────┘ └───┘
typ └─────┘└┘└─────────────┘ └───┘└┘
doc └─────┘ └─────────────┘ └───┘
txt └─────┘ └─────────────┘ └───┘
par └─────┘ └─────────────┘ └───┘
pid ┴ └─────────────┘ └─┘
st ───────────────────────────────────────
425 simp only [term.val_add, term.val_mul, cancel];
id └──────────┘ └──────────┘ └────┘
src └─────────┘└──────────┘└┘└──────────┘└┘└────┘┴
typ └─────────┘└──────────┘└┘└──────────┘└┘└────┘┴
doc └─────────┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ ┴
st ────────────────────────────────────────────────────
426 rw [← h1, mul_zero, zero_add],
id └┘ └──────┘ └──────┘
src └────┘ └┘└──────┘└┘└──────┘┴
typ └────┘└┘└┘└──────┘└┘└──────┘┴
doc └────┘ └┘ └┘ ┴
txt └────┘ └┘ └┘ ┴
par └────┘ └┘ └┘ ┴
pid └──┘ └┘ └┘ ┴
st ───────┘└──┘└────────┘└────────┘┴└─
427 { apply h3 _ h4 },
id └┘ └┘
src └────┘ └─┘ ┴
typ └────┘└┘└─┘└┘┴
doc └────┘ └─┘ ┴
txt └────┘ └─┘ ┴
par └────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ─────┘└────────────┘└┘└
428 { apply h2 _ h4 }
id └┘ └┘
src └────┘ └─┘ ┴
typ └────┘└┘└─┘└┘┴
doc └────┘ └─┘ ┴
txt └────┘ └─┘ ┴
par └────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ───────────────────┘└─
429 end
st ────┘
430
431 lemma unsat_of_unsat_eq_elim (ee : list ee) (c : clause) :
id └──┘ └┘ └────┘
src └──┘ └┘ └────┘
typ └──┘ └┘ └────┘
432 (eq_elim ee c).unsat → c.unsat :=
id └─────┘ └┘ ┴ └───┘ ┴└────┘
src └─────┘ └───┘ └────┘
typ └─────┘ └┘ ┴ └───┘ ┴└────┘
433 by {intros h1 h2, apply h1, apply sat_eq_elim h2}
id └─────────┘ └┘
src └──────────┘ └────┘ └────┘└─────────┘┴
typ └──────────┘ └────┘ └────┘└─────────┘┴└┘
doc └──────────┘ └────┘ └────┘ ┴
txt └──────────┘ └────┘ └────┘ ┴
par └──────────┘ └────┘ └────┘ ┴
pid └────┘ ┴ ┴ ┴
st └────────────┘└────────┘└────────────────────┘└┘
434
435 end omega